src/HOL/Tools/typedef_package.ML

   val typedef: (bool * string) * (bstring * string list * mixfix) * string
     * (string * string) option -> theory -> Proof.state
   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 =
 struct
 

 
 fun err_in_typedef msg name =
   cat_error msg ("The error(s) above occurred in typedef " ^ quote name);
 
 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";
     val ctxt = ProofContext.init thy;

             Rep_name = full Rep_name, Abs_name = full Abs_name,
               type_definition = type_definition, set_def = set_def,
               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 *)
 
     fun show_names pairs = commas_quote (map fst pairs);

   in (set, goal, goal_pat, typedef_result) end
   handle ERROR msg => err_in_typedef msg name;
 
 
 (* 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 =
   let

     val non_empty = Goal.prove_global thy [] [] goal (K tac) handle ERROR msg =>
       cat_error msg ("Failed to prove non-emptiness of " ^ quote (string_of_term set));
   in
     thy
     |> typedef_result non_empty
-    |-> (fn (a, info) => TypedefInterpretation.data a #> pair (a, info))
   end;
 
 in
 
 val add_typedef = gen_typedef Syntax.read_term;

 
 val _ =
   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)));
 
-end;
-
-end;
+val setup = TypedefInterpretation.init;
+
+end;
+
+end;