src/HOL/Tools/typedef_package.ML

     val typedefC =
       Const (type_definitionN, (newT --> oldT) --> (oldT --> newT) --> setT --> HOLogic.boolT);
     val typedef_prop = HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set');
 
     (*theory extender*)
-    fun do_typedef theory =
+    fun do_typedef super_theory theory =
       theory
-      |> Theory.assert_super thy
+      |> Theory.assert_super super_theory
       |> add_typedecls [(t, vs, mx)]
       |> Theory.add_consts_i
        ((if no_def then [] else [(name, setT, NoSyn)]) @
         [(Rep_name, newT --> oldT, NoSyn),
          (Abs_name, oldT --> newT, NoSyn)])

 
 fun gen_add_typedef prep_term no_def name typ set names thms tac thy =
   let
     val (cset, _, do_typedef) = prepare_typedef prep_term no_def name typ set thy;
     val result = prove_nonempty thy cset (names, thms, tac);
-  in check_nonempty cset result; thy |> do_typedef |> #1 end;
+  in check_nonempty cset result; thy |> do_typedef thy |> #1 end;
 
 val add_typedef = gen_add_typedef read_term false;
 val add_typedef_i = gen_add_typedef cert_term false;
 val add_typedef_i_no_def = gen_add_typedef cert_term true;
 

 fun gen_typedef_proof prep_term ((name, typ, set), comment) int thy =
   let
     val (cset, cset_pat, do_typedef) = prepare_typedef prep_term false name typ set thy;
     val goal = Thm.term_of (goal_nonempty true cset);
     val goal_pat = Thm.term_of (goal_nonempty true cset_pat);
-  in
-    thy
-    |> IsarThy.theorem_i ((("", [typedef_attribute cset do_typedef]),
+    val test_thy = Theory.copy thy;
+  in
+    test_thy |> do_typedef test_thy;  (*preview errors!*)
+    thy |> IsarThy.theorem_i ((("", [typedef_attribute cset (do_typedef thy)]),
       (goal, ([goal_pat], []))), comment) int
   end;
 
 val typedef_proof = gen_typedef_proof read_term;
 val typedef_proof_i = gen_typedef_proof cert_term;