check result against certified prop, i.e. admit non-normal statements;
authorwenzelm
Thu May 11 21:46:17 2006 +0200 (2006-05-11)
changeset 19619ee1104f972a4
parent 19618 9050a3b01e62
child 19620 ccd6de95f4a6
check result against certified prop, i.e. admit non-normal statements;
src/Pure/goal.ML
     1.1 --- a/src/Pure/goal.ML	Thu May 11 19:19:33 2006 +0200
     1.2 +++ b/src/Pure/goal.ML	Thu May 11 21:46:17 2006 +0200
     1.3 @@ -139,13 +139,16 @@
     1.4      val casms = map cert_safe asms;
     1.5      val prems = map (norm_hhf o Thm.assume) casms;
     1.6  
     1.7 -    val goal = init (cert_safe prop);
     1.8 +    val cprop = cert_safe prop;
     1.9 +    val goal = init cprop;
    1.10      val goal' = case SINGLE (tac prems) goal of SOME goal' => goal' | _ => err "Tactic failed.";
    1.11      val raw_result = finish goal' handle THM (msg, _, _) => err msg;
    1.12  
    1.13      val prop' = Thm.prop_of raw_result;
    1.14 -    val _ = conditional (not (Pattern.matches thy (Envir.beta_norm prop, prop'))) (fn () =>
    1.15 -      err ("Proved a different theorem: " ^ Sign.string_of_term thy prop'));
    1.16 +    val _ =
    1.17 +      if not (Pattern.matches thy (Envir.beta_norm (Thm.term_of cprop), prop'))
    1.18 +      then err ("Proved a different theorem: " ^ Sign.string_of_term thy prop')
    1.19 +      else ();
    1.20    in
    1.21      hd (Conjunction.elim_precise [length props] raw_result)
    1.22      |> map