src/HOL/Tools/typecopy_package.ML
changeset 24711 e8bba7723858
parent 24626 85eceef2edc7
child 25489 5b0625f6e324
     1.1 --- a/src/HOL/Tools/typecopy_package.ML	Tue Sep 25 13:42:59 2007 +0200
     1.2 +++ b/src/HOL/Tools/typecopy_package.ML	Tue Sep 25 15:34:35 2007 +0200
     1.3 @@ -19,8 +19,7 @@
     1.4      -> theory -> (string * info) * theory
     1.5    val get_typecopies: theory -> string list
     1.6    val get_typecopy_info: theory -> string -> info option
     1.7 -  type interpretator = string * info -> theory -> theory
     1.8 -  val add_interpretator: interpretator -> theory -> theory
     1.9 +  val interpretation: (string * info -> theory -> theory) -> theory -> theory
    1.10    val get_spec: theory -> string -> (string * sort) list * (string * typ list) list
    1.11    val get_eq: theory -> string -> thm
    1.12    val print_typecopies: theory -> unit
    1.13 @@ -41,8 +40,6 @@
    1.14    proj_def: thm
    1.15  };
    1.16  
    1.17 -structure TypecopyInterpretator = TheoryInterpretatorFun(struct type T = string; val eq = op = end);
    1.18 -
    1.19  structure TypecopyData = TheoryDataFun
    1.20  (
    1.21    type T = info Symtab.table;
    1.22 @@ -71,12 +68,12 @@
    1.23  val get_typecopy_info = Symtab.lookup o TypecopyData.get;
    1.24  
    1.25  
    1.26 -(* interpretator management *)
    1.27 +(* interpretation *)
    1.28  
    1.29 -type interpretator = string * info -> theory -> theory;
    1.30 +structure TypecopyInterpretation = InterpretationFun(type T = string val eq = op =);
    1.31  
    1.32 -fun add_interpretator interp = TypecopyInterpretator.add_interpretator
    1.33 -  (fold (fn tyco => fn thy => interp (tyco, (the o get_typecopy_info thy) tyco) thy));
    1.34 +fun interpretation interp = TypecopyInterpretation.interpretation
    1.35 +  (fn tyco => fn thy => interp (tyco, (the o get_typecopy_info thy) tyco) thy);
    1.36  
    1.37  
    1.38  (* add a type copy *)
    1.39 @@ -108,7 +105,7 @@
    1.40          in
    1.41            thy
    1.42            |> (TypecopyData.map o Symtab.update_new) (tyco, info)
    1.43 -          |> TypecopyInterpretator.add_those [tyco]
    1.44 +          |> TypecopyInterpretation.data tyco
    1.45            |> pair (tyco, info)
    1.46          end
    1.47    in
    1.48 @@ -137,10 +134,10 @@
    1.49    in (vs, [(constr, [typ])]) end;
    1.50  
    1.51  
    1.52 -(* interpretator for projection function code *)
    1.53 +(* interpretation for projection function code *)
    1.54  
    1.55 -fun add_project (_ , {proj_def, ...} : info) = Code.add_default_func proj_def;
    1.56 +fun add_project (_, {proj_def, ...} : info) = Code.add_default_func proj_def;
    1.57  
    1.58 -val setup = TypecopyInterpretator.init #> add_interpretator add_project;
    1.59 +val setup = TypecopyInterpretation.init #> interpretation add_project;
    1.60  
    1.61  end;