# HG changeset patch
# User kuncar
# Date 1393261959 -3600
# Node ID 1c2cfc06c96acd9a10031128a54664d641f1f279
# Parent  f3a2931a66568dc05270d83e0c4334417f2c980f
don't be so aggresive for a public test function and raise only BAD_THM instead of ERROR

diff -r f3a2931a6656 -r 1c2cfc06c96a src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon Feb 24 18:12:39 2014 +0100
+++ b/src/Pure/Isar/code.ML	Mon Feb 24 18:12:39 2014 +0100
@@ -548,7 +548,7 @@
       else error ("Type arguments do not satisfy sort constraints of abstype certificate.");
   in (thm, tyco) end;
 
-fun assert_eqn thy = error_thm (gen_assert_eqn thy true) thy;
+fun assert_eqn thy = gen_assert_eqn thy true;
 
 fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (Proof_Context.init_global thy);
 
@@ -752,7 +752,7 @@
       let
         val thy = Proof_Context.theory_of ctxt;
         val eqns = burrow_fst (canonize_thms thy) raw_eqns;
-        val _ = map (assert_eqn thy) eqns;
+        val _ = map (error_thm (assert_eqn thy) thy) eqns;
         val (thms, propers) = split_list eqns;
         val _ = map (fn thm => if c = const_eqn thy thm then ()
           else error ("Wrong head of code equation,\nexpected constant "