--- a/src/Pure/Isar/proof.ML Mon Jun 12 21:19:00 2006 +0200
+++ b/src/Pure/Isar/proof.ML Mon Jun 12 21:19:02 2006 +0200
@@ -483,7 +483,7 @@
val (results, th) = `(Conjunction.elim_precise (map length propss)) (Goal.conclude goal)
handle THM _ => error ("Lost goal structure:\n" ^ string_of_thm goal);
- val _ = Pattern.matches_seq thy (flat propss) (map Thm.prop_of (flat results)) orelse
+ val _ = Unify.matches_list thy (flat propss) (map Thm.prop_of (flat results)) orelse
error ("Proved a different theorem:\n" ^ string_of_thm th);
in results end;
--- a/src/Pure/goal.ML Mon Jun 12 21:19:00 2006 +0200
+++ b/src/Pure/goal.ML Mon Jun 12 21:19:02 2006 +0200
@@ -105,7 +105,7 @@
fun compose_hhf_tac th i = PRIMSEQ (compose_hhf th i);
fun comp_hhf tha thb =
- (case Seq.chop (2, compose_hhf tha 1 thb) of
+ (case Seq.chop 2 (compose_hhf tha 1 thb) of
([th], _) => th
| ([], _) => raise THM ("comp_hhf: no unifiers", 1, [tha, thb])
| _ => raise THM ("comp_hhf: multiple unifiers", 1, [tha, thb]));
@@ -144,7 +144,7 @@
| SOME res => res);
val [results] =
Conjunction.elim_precise [length props] (finish res) handle THM (msg, _, _) => err msg;
- val _ = Pattern.matches_seq thy (map (Thm.term_of o cert_safe) props) (map Thm.prop_of results)
+ val _ = Unify.matches_list thy (map (Thm.term_of o cert_safe) props) (map Thm.prop_of results)
orelse err ("Proved a different theorem: " ^ Sign.string_of_term thy (Thm.prop_of res));
in
results |> map