modernized functor/structures Interpretation;

--- a/src/HOL/Tools/Datatype/datatype.ML	Thu Oct 29 16:09:41 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Thu Oct 29 16:15:33 2009 +0100
@@ -263,7 +263,7 @@
 
 (** abstract theory extensions relative to a datatype characterisation **)
 
-structure Datatype_Interpretation = InterpretationFun
+structure Datatype_Interpretation = Interpretation
   (type T = config * string list val eq: T * T -> bool = eq_snd op =);
 fun interpretation f = Datatype_Interpretation.interpretation (uncurry f);
 

--- a/src/HOL/Tools/typecopy.ML	Thu Oct 29 16:09:41 2009 +0100
+++ b/src/HOL/Tools/typecopy.ML	Thu Oct 29 16:15:33 2009 +0100
@@ -44,8 +44,8 @@
 
 (* interpretation of type copies *)
 
-structure TypecopyInterpretation = InterpretationFun(type T = string val eq = op =);
-val interpretation = TypecopyInterpretation.interpretation;
+structure Typecopy_Interpretation = Interpretation(type T = string val eq = op =);
+val interpretation = Typecopy_Interpretation.interpretation;
 
 
 (* introducing typecopies *)
@@ -76,7 +76,7 @@
         in
           thy
           |> (TypecopyData.map o Symtab.update_new) (tyco, info)
-          |> TypecopyInterpretation.data tyco
+          |> Typecopy_Interpretation.data tyco
           |> pair (tyco, info)
         end
   in
@@ -126,7 +126,7 @@
   end;
 
 val setup =
-  TypecopyInterpretation.init
+  Typecopy_Interpretation.init
   #> interpretation add_default_code
 
 end;

--- 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;

--- a/src/Pure/Isar/code.ML	Thu Oct 29 16:09:41 2009 +0100
+++ b/src/Pure/Isar/code.ML	Thu Oct 29 16:15:33 2009 +0100
@@ -639,7 +639,8 @@
 
 (* datatypes *)
 
-structure Type_Interpretation = InterpretationFun(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
+structure Type_Interpretation =
+  Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
 
 fun add_datatype raw_cs thy =
   let

--- a/src/Pure/interpretation.ML	Thu Oct 29 16:09:41 2009 +0100
+++ b/src/Pure/interpretation.ML	Thu Oct 29 16:15:33 2009 +0100
@@ -13,7 +13,7 @@
   val init: theory -> theory
 end;
 
-functor InterpretationFun(type T val eq: T * T -> bool): INTERPRETATION =
+functor Interpretation(type T val eq: T * T -> bool): INTERPRETATION =
 struct
 
 type T = T;