# HG changeset patch
# User wenzelm
# Date 977227609 -3600
# Node ID ec197510165a5b73c93ed0ef014ecaa815e926f0
# Parent  76d7f6c9a14c2a42a8ca5c8a381389e55ade35db
improved errors;

diff -r 76d7f6c9a14c -r ec197510165a src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Mon Dec 18 16:45:17 2000 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Tue Dec 19 13:06:49 2000 +0100
@@ -154,9 +154,9 @@
     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)]) @
@@ -219,7 +219,7 @@
   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;
@@ -236,9 +236,10 @@
     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);
+    val test_thy = Theory.copy thy;
   in
-    thy
-    |> IsarThy.theorem_i ((("", [typedef_attribute cset do_typedef]),
+    test_thy |> do_typedef test_thy;  (*preview errors!*)
+    thy |> IsarThy.theorem_i ((("", [typedef_attribute cset (do_typedef thy)]),
       (goal, ([goal_pat], []))), comment) int
   end;