src/Pure/goal.ML
changeset 19862 7f29aa958b72
parent 19774 5fe7731d0836
child 20056 0698a403a066
     1.1 --- a/src/Pure/goal.ML	Mon Jun 12 21:19:00 2006 +0200
     1.2 +++ b/src/Pure/goal.ML	Mon Jun 12 21:19:02 2006 +0200
     1.3 @@ -105,7 +105,7 @@
     1.4  fun compose_hhf_tac th i = PRIMSEQ (compose_hhf th i);
     1.5  
     1.6  fun comp_hhf tha thb =
     1.7 -  (case Seq.chop (2, compose_hhf tha 1 thb) of
     1.8 +  (case Seq.chop 2 (compose_hhf tha 1 thb) of
     1.9      ([th], _) => th
    1.10    | ([], _) => raise THM ("comp_hhf: no unifiers", 1, [tha, thb])
    1.11    | _  => raise THM ("comp_hhf: multiple unifiers", 1, [tha, thb]));
    1.12 @@ -144,7 +144,7 @@
    1.13        | SOME res => res);
    1.14      val [results] =
    1.15        Conjunction.elim_precise [length props] (finish res) handle THM (msg, _, _) => err msg;
    1.16 -    val _ = Pattern.matches_seq thy (map (Thm.term_of o cert_safe) props) (map Thm.prop_of results)
    1.17 +    val _ = Unify.matches_list thy (map (Thm.term_of o cert_safe) props) (map Thm.prop_of results)
    1.18        orelse err ("Proved a different theorem: " ^ Sign.string_of_term thy (Thm.prop_of res));
    1.19    in
    1.20      results |> map