Unify.matches_list;

--- 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