equal
deleted
inserted
replaced
103 |
103 |
104 fun mk_all_internal ctxt (y, z) t = |
104 fun mk_all_internal ctxt (y, z) t = |
105 let |
105 let |
106 val frees = Frees.build (t |> Term.fold_aterms (fn Free v => Frees.add_set v | _ => I)); |
106 val frees = Frees.build (t |> Term.fold_aterms (fn Free v => Frees.add_set v | _ => I)); |
107 val T = |
107 val T = |
108 (case Frees.get_first (fn ((x, T), _) => if x = z then SOME T else NONE) frees of |
108 Frees.get_first (fn ((x, T), _) => if x = z then SOME T else NONE) frees |
109 SOME T => T |
109 |> \<^if_none>\<open>the_default dummyT (Variable.default_type ctxt z)\<close>; |
110 | NONE => the_default dummyT (Variable.default_type ctxt z)); |
|
111 in Logic.all_const T $ Term.lambda_name (y, Free (z, T)) t end; |
110 in Logic.all_const T $ Term.lambda_name (y, Free (z, T)) t end; |
112 |
111 |
113 fun prepare_clause prep_var parse_prop mk_all ctxt thesis raw_vars raw_props = |
112 fun prepare_clause prep_var parse_prop mk_all ctxt thesis raw_vars raw_props = |
114 let |
113 let |
115 val ((xs', vars), ctxt') = ctxt |
114 val ((xs', vars), ctxt') = ctxt |