Unify.matches_list;
authorwenzelm
Mon Jun 12 21:19:02 2006 +0200 (2006-06-12)
changeset 198627f29aa958b72
parent 19861 620d90091788
child 19863 3a4ca87efdc5
Unify.matches_list;
src/Pure/Isar/proof.ML
src/Pure/goal.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Mon Jun 12 21:19:00 2006 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Mon Jun 12 21:19:02 2006 +0200
     1.3 @@ -483,7 +483,7 @@
     1.4  
     1.5      val (results, th) = `(Conjunction.elim_precise (map length propss)) (Goal.conclude goal)
     1.6        handle THM _ => error ("Lost goal structure:\n" ^ string_of_thm goal);
     1.7 -    val _ = Pattern.matches_seq thy (flat propss) (map Thm.prop_of (flat results)) orelse
     1.8 +    val _ = Unify.matches_list thy (flat propss) (map Thm.prop_of (flat results)) orelse
     1.9        error ("Proved a different theorem:\n" ^ string_of_thm th);
    1.10    in results end;
    1.11  
     2.1 --- a/src/Pure/goal.ML	Mon Jun 12 21:19:00 2006 +0200
     2.2 +++ b/src/Pure/goal.ML	Mon Jun 12 21:19:02 2006 +0200
     2.3 @@ -105,7 +105,7 @@
     2.4  fun compose_hhf_tac th i = PRIMSEQ (compose_hhf th i);
     2.5  
     2.6  fun comp_hhf tha thb =
     2.7 -  (case Seq.chop (2, compose_hhf tha 1 thb) of
     2.8 +  (case Seq.chop 2 (compose_hhf tha 1 thb) of
     2.9      ([th], _) => th
    2.10    | ([], _) => raise THM ("comp_hhf: no unifiers", 1, [tha, thb])
    2.11    | _  => raise THM ("comp_hhf: multiple unifiers", 1, [tha, thb]));
    2.12 @@ -144,7 +144,7 @@
    2.13        | SOME res => res);
    2.14      val [results] =
    2.15        Conjunction.elim_precise [length props] (finish res) handle THM (msg, _, _) => err msg;
    2.16 -    val _ = Pattern.matches_seq thy (map (Thm.term_of o cert_safe) props) (map Thm.prop_of results)
    2.17 +    val _ = Unify.matches_list thy (map (Thm.term_of o cert_safe) props) (map Thm.prop_of results)
    2.18        orelse err ("Proved a different theorem: " ^ Sign.string_of_term thy (Thm.prop_of res));
    2.19    in
    2.20      results |> map