interpretation of typedefs

--- a/src/HOL/Tools/typedef_package.ML	Wed Dec 05 14:15:45 2007 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Wed Dec 05 14:15:48 2007 +0100
@@ -24,6 +24,7 @@
   val typedef_i: (bool * string) * (bstring * string list * mixfix) * term
     * (string * string) option -> theory -> Proof.state
   val interpretation: (string -> theory -> theory) -> theory -> theory
+  val setup: theory -> theory
 end;
 
 structure TypedefPackage: TYPEDEF_PACKAGE =
@@ -81,6 +82,9 @@
 
 fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
 
+structure TypedefInterpretation = InterpretationFun(type T = string val eq = op =);
+val interpretation = TypedefInterpretation.interpretation;
+
 fun prepare_typedef prep_term def name (t, vs, mx) raw_set opt_morphs thy =
   let
     val _ = Theory.requires thy "Typedef" "typedefs";
@@ -177,8 +181,12 @@
               Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
               Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
             Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct};
-          val thy3 = thy2 |> put_info full_tname info;
-        in ((full_tname, info), thy3) end);
+        in
+          thy2
+          |> put_info full_tname info
+          |> TypedefInterpretation.data full_tname
+          |> pair (full_tname, info)
+        end);
 
 
     (* errors *)
@@ -215,9 +223,6 @@
 
 (* add_typedef interfaces *)
 
-structure TypedefInterpretation = InterpretationFun(type T = string val eq = op =);
-val interpretation = TypedefInterpretation.interpretation;
-
 local
 
 fun gen_typedef prep_term def opt_name typ set opt_morphs tac thy =
@@ -232,7 +237,6 @@
   in
     thy
     |> typedef_result non_empty
-    |-> (fn (a, info) => TypedefInterpretation.data a #> pair (a, info))
   end;
 
 in
@@ -283,6 +287,8 @@
   OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal
     (typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef)));
 
+val setup = TypedefInterpretation.init;
+
 end;
 
 end;

--- a/src/HOL/Typedef.thy	Wed Dec 05 14:15:45 2007 +0100
+++ b/src/HOL/Typedef.thy	Wed Dec 05 14:15:48 2007 +0100
@@ -109,7 +109,8 @@
 use "Tools/typedef_codegen.ML"
 
 setup {*
-  TypecopyPackage.setup
+  TypedefPackage.setup
+  #> TypecopyPackage.setup
   #> TypedefCodegen.setup
 *}