src/Pure/Isar/code.ML

       allow_consts = false, allow_pats = false } thm (lhs, rhs);
     val _ = if forall2 (fn T => fn (_, sort) => Sign.of_sort thy (T, sort)) Ts vs' then ()
       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);
 
 fun mk_eqn thy = error_thm (gen_assert_eqn thy false) thy o
   apfst (meta_rewrite thy);

 fun cert_of_eqns ctxt c [] = Equations (dummy_thm ctxt c, [])
   | cert_of_eqns ctxt c raw_eqns = 
       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 "
             ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy thm)) thms;
         fun tvars_of T = rev (Term.add_tvarsT T []);