# HG changeset patch
# User wenzelm
# Date 1147376777 -7200
# Node ID ee1104f972a44cdb37cc0eb83b39ee303bdc3b69
# Parent  9050a3b01e626da78173a17931920d3c630531b2
check result against certified prop, i.e. admit non-normal statements;

diff -r 9050a3b01e62 -r ee1104f972a4 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Thu May 11 19:19:33 2006 +0200
+++ b/src/Pure/goal.ML	Thu May 11 21:46:17 2006 +0200
@@ -139,13 +139,16 @@
     val casms = map cert_safe asms;
     val prems = map (norm_hhf o Thm.assume) casms;
 
-    val goal = init (cert_safe prop);
+    val cprop = cert_safe prop;
+    val goal = init cprop;
     val goal' = case SINGLE (tac prems) goal of SOME goal' => goal' | _ => err "Tactic failed.";
     val raw_result = finish goal' handle THM (msg, _, _) => err msg;
 
     val prop' = Thm.prop_of raw_result;
-    val _ = conditional (not (Pattern.matches thy (Envir.beta_norm prop, prop'))) (fn () =>
-      err ("Proved a different theorem: " ^ Sign.string_of_term thy prop'));
+    val _ =
+      if not (Pattern.matches thy (Envir.beta_norm (Thm.term_of cprop), prop'))
+      then err ("Proved a different theorem: " ^ Sign.string_of_term thy prop')
+      else ();
   in
     hd (Conjunction.elim_precise [length props] raw_result)
     |> map