equal
deleted
inserted
replaced
105 in thA RS (cterm_instantiate ct_pairs thB) end) () of |
105 in thA RS (cterm_instantiate ct_pairs thB) end) () of |
106 SOME th => th |
106 SOME th => th |
107 | NONE => raise THM ("first_order_resolve", 0, [thA, thB])) |
107 | NONE => raise THM ("first_order_resolve", 0, [thA, thB])) |
108 |
108 |
109 fun flexflex_first_order th = |
109 fun flexflex_first_order th = |
110 case (tpairs_of th) of |
110 case Thm.tpairs_of th of |
111 [] => th |
111 [] => th |
112 | pairs => |
112 | pairs => |
113 let val thy = theory_of_thm th |
113 let val thy = theory_of_thm th |
114 val (tyenv, tenv) = |
114 val (tyenv, tenv) = |
115 fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty) |
115 fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty) |