src/Pure/goal.ML
changeset 19774 5fe7731d0836
parent 19619 ee1104f972a4
child 19862 7f29aa958b72
     1.1 --- a/src/Pure/goal.ML	Mon Jun 05 19:54:12 2006 +0200
     1.2 +++ b/src/Pure/goal.ML	Mon Jun 05 21:54:20 2006 +0200
     1.3 @@ -128,7 +128,6 @@
     1.4      fun err msg = cat_error msg
     1.5        ("The error(s) above occurred for the goal statement:\n" ^
     1.6          Sign.string_of_term thy (Term.list_all_free (params, statement)));
     1.7 -
     1.8      fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm t)
     1.9        handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
    1.10  
    1.11 @@ -139,19 +138,16 @@
    1.12      val casms = map cert_safe asms;
    1.13      val prems = map (norm_hhf o Thm.assume) casms;
    1.14  
    1.15 -    val cprop = cert_safe prop;
    1.16 -    val goal = init cprop;
    1.17 -    val goal' = case SINGLE (tac prems) goal of SOME goal' => goal' | _ => err "Tactic failed.";
    1.18 -    val raw_result = finish goal' handle THM (msg, _, _) => err msg;
    1.19 -
    1.20 -    val prop' = Thm.prop_of raw_result;
    1.21 -    val _ =
    1.22 -      if not (Pattern.matches thy (Envir.beta_norm (Thm.term_of cprop), prop'))
    1.23 -      then err ("Proved a different theorem: " ^ Sign.string_of_term thy prop')
    1.24 -      else ();
    1.25 +    val res =
    1.26 +      (case SINGLE (tac prems) (init (cert_safe prop)) of
    1.27 +        NONE => err "Tactic failed."
    1.28 +      | SOME res => res);
    1.29 +    val [results] =
    1.30 +      Conjunction.elim_precise [length props] (finish res) handle THM (msg, _, _) => err msg;
    1.31 +    val _ = Pattern.matches_seq thy (map (Thm.term_of o cert_safe) props) (map Thm.prop_of results)
    1.32 +      orelse err ("Proved a different theorem: " ^ Sign.string_of_term thy (Thm.prop_of res));
    1.33    in
    1.34 -    hd (Conjunction.elim_precise [length props] raw_result)
    1.35 -    |> map
    1.36 +    results |> map
    1.37        (Drule.implies_intr_list casms
    1.38          #> Drule.forall_intr_list cparams
    1.39          #> norm_hhf