Lines Matching defs:Term
241 String.concat ["(Term.prim_mk_const { Name = ",
460 fun Term q = absyn_to_term (term_grammar()) (Absyn q)
465 Term (case (Lib.front_last qtm)
855 CLR_OVL s :: map (fn t => OVERLOAD_ON(s,t)) (Term.decls s)
896 Lib.can Term.prim_mk_const{Name="NUMERAL", Thy="arithmetic"}
906 case Term.decls s of
953 case Term.decls s of
969 let val declared = Term.all_consts()
970 val names = map (fst o Term.dest_const) declared
976 val (ok_names, bad_names) = partition (not o null o Term.decls) sl