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 (case Frees.get_first (fn ((x, T), _) => if x = z then SOME T else NONE) frees of |
109 SOME T => T |
109 SOME T => T |
110 | NONE => the_default dummyT (Variable.default_type ctxt z)); |
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; |
111 in Logic.all_const T $ Term.lambda_name (y, Free (z, T)) t end; |
112 |
112 |
113 fun prepare_clause prep_var parse_prop mk_all ctxt thesis raw_vars raw_props = |
113 fun prepare_clause prep_var parse_prop mk_all ctxt thesis raw_vars raw_props = |