modernized functor/structures Interpretation;
authorwenzelm
Thu Oct 29 16:15:33 2009 +0100 (2009-10-29)
changeset 3331453d49370f7af
parent 33313 f6acebef3ea1
child 33315 784c1b09d485
modernized functor/structures Interpretation;
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/typecopy.ML
src/HOL/Tools/typedef.ML
src/Pure/Isar/code.ML
src/Pure/interpretation.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Thu Oct 29 16:09:41 2009 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Thu Oct 29 16:15:33 2009 +0100
     1.3 @@ -263,7 +263,7 @@
     1.4  
     1.5  (** abstract theory extensions relative to a datatype characterisation **)
     1.6  
     1.7 -structure Datatype_Interpretation = InterpretationFun
     1.8 +structure Datatype_Interpretation = Interpretation
     1.9    (type T = config * string list val eq: T * T -> bool = eq_snd op =);
    1.10  fun interpretation f = Datatype_Interpretation.interpretation (uncurry f);
    1.11  
     2.1 --- a/src/HOL/Tools/typecopy.ML	Thu Oct 29 16:09:41 2009 +0100
     2.2 +++ b/src/HOL/Tools/typecopy.ML	Thu Oct 29 16:15:33 2009 +0100
     2.3 @@ -44,8 +44,8 @@
     2.4  
     2.5  (* interpretation of type copies *)
     2.6  
     2.7 -structure TypecopyInterpretation = InterpretationFun(type T = string val eq = op =);
     2.8 -val interpretation = TypecopyInterpretation.interpretation;
     2.9 +structure Typecopy_Interpretation = Interpretation(type T = string val eq = op =);
    2.10 +val interpretation = Typecopy_Interpretation.interpretation;
    2.11  
    2.12  
    2.13  (* introducing typecopies *)
    2.14 @@ -76,7 +76,7 @@
    2.15          in
    2.16            thy
    2.17            |> (TypecopyData.map o Symtab.update_new) (tyco, info)
    2.18 -          |> TypecopyInterpretation.data tyco
    2.19 +          |> Typecopy_Interpretation.data tyco
    2.20            |> pair (tyco, info)
    2.21          end
    2.22    in
    2.23 @@ -126,7 +126,7 @@
    2.24    end;
    2.25  
    2.26  val setup =
    2.27 -  TypecopyInterpretation.init
    2.28 +  Typecopy_Interpretation.init
    2.29    #> interpretation add_default_code
    2.30  
    2.31  end;
     3.1 --- a/src/HOL/Tools/typedef.ML	Thu Oct 29 16:09:41 2009 +0100
     3.2 +++ b/src/HOL/Tools/typedef.ML	Thu Oct 29 16:15:33 2009 +0100
     3.3 @@ -53,8 +53,8 @@
     3.4  
     3.5  fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
     3.6  
     3.7 -structure TypedefInterpretation = InterpretationFun(type T = string val eq = op =);
     3.8 -val interpretation = TypedefInterpretation.interpretation;
     3.9 +structure Typedef_Interpretation = Interpretation(type T = string val eq = op =);
    3.10 +val interpretation = Typedef_Interpretation.interpretation;
    3.11  
    3.12  fun prepare_typedef prep_term def name (t, vs, mx) raw_set opt_morphs thy =
    3.13    let
    3.14 @@ -169,7 +169,7 @@
    3.15          in
    3.16            thy2
    3.17            |> put_info full_tname info
    3.18 -          |> TypedefInterpretation.data full_tname
    3.19 +          |> Typedef_Interpretation.data full_tname
    3.20            |> pair (full_tname, info)
    3.21          end);
    3.22  
    3.23 @@ -264,6 +264,6 @@
    3.24  end;
    3.25  
    3.26  
    3.27 -val setup = TypedefInterpretation.init;
    3.28 +val setup = Typedef_Interpretation.init;
    3.29  
    3.30  end;
     4.1 --- a/src/Pure/Isar/code.ML	Thu Oct 29 16:09:41 2009 +0100
     4.2 +++ b/src/Pure/Isar/code.ML	Thu Oct 29 16:15:33 2009 +0100
     4.3 @@ -639,7 +639,8 @@
     4.4  
     4.5  (* datatypes *)
     4.6  
     4.7 -structure Type_Interpretation = InterpretationFun(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
     4.8 +structure Type_Interpretation =
     4.9 +  Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
    4.10  
    4.11  fun add_datatype raw_cs thy =
    4.12    let
     5.1 --- a/src/Pure/interpretation.ML	Thu Oct 29 16:09:41 2009 +0100
     5.2 +++ b/src/Pure/interpretation.ML	Thu Oct 29 16:15:33 2009 +0100
     5.3 @@ -13,7 +13,7 @@
     5.4    val init: theory -> theory
     5.5  end;
     5.6  
     5.7 -functor InterpretationFun(type T val eq: T * T -> bool): INTERPRETATION =
     5.8 +functor Interpretation(type T val eq: T * T -> bool): INTERPRETATION =
     5.9  struct
    5.10  
    5.11  type T = T;