src/HOL/Tools/typedef.ML

--- a/src/HOL/Tools/typedef.ML	Thu Oct 29 16:09:41 2009 +0100
+++ b/src/HOL/Tools/typedef.ML	Thu Oct 29 16:15:33 2009 +0100
@@ -53,8 +53,8 @@
 
 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;
+structure Typedef_Interpretation = Interpretation(type T = string val eq = op =);
+val interpretation = Typedef_Interpretation.interpretation;
 
 fun prepare_typedef prep_term def name (t, vs, mx) raw_set opt_morphs thy =
   let
@@ -169,7 +169,7 @@
         in
           thy2
           |> put_info full_tname info
-          |> TypedefInterpretation.data full_tname
+          |> Typedef_Interpretation.data full_tname
           |> pair (full_tname, info)
         end);
 
@@ -264,6 +264,6 @@
 end;
 
 
-val setup = TypedefInterpretation.init;
+val setup = Typedef_Interpretation.init;
 
 end;