src/HOL/Tools/datatype_package.ML
changeset 24711 e8bba7723858
parent 24699 c6674504103f
child 24712 64ed05609568
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Sep 25 13:42:59 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Sep 25 15:34:35 2007 +0200
     1.3 @@ -65,7 +65,7 @@
     1.4    val datatype_of_case : theory -> string -> DatatypeAux.datatype_info option
     1.5    val get_datatype_spec : theory -> string -> ((string * sort) list * (string * typ list) list) option
     1.6    val get_datatype_constrs : theory -> string -> (string * typ) list option
     1.7 -  val add_interpretator: (string list -> theory -> theory) -> theory -> theory
     1.8 +  val interpretation: (string list -> theory -> theory) -> theory -> theory
     1.9    val print_datatypes : theory -> unit
    1.10    val make_case :  Proof.context -> bool -> string list -> term ->
    1.11      (term * term) list -> term * (term * (int * bool)) list
    1.12 @@ -134,7 +134,7 @@
    1.13  
    1.14  fun get_datatype_descr thy dtco =
    1.15    get_datatype thy dtco
    1.16 -  |> Option.map (fn info as { descr, index, ... } => 
    1.17 +  |> Option.map (fn info as { descr, index, ... } =>
    1.18         (info, (((fn SOME (_, dtys, cos) => (dtys, cos)) o AList.lookup (op =) descr) index)));
    1.19  
    1.20  fun get_datatype_spec thy dtco =
    1.21 @@ -210,7 +210,7 @@
    1.22  
    1.23  in
    1.24  
    1.25 -fun gen_induct_tac inst_tac (varss, opt_rule) i state = 
    1.26 +fun gen_induct_tac inst_tac (varss, opt_rule) i state =
    1.27    SUBGOAL (fn (Bi,_) =>
    1.28    let
    1.29      val (rule, rule_name) =
    1.30 @@ -219,7 +219,7 @@
    1.31          | NONE =>
    1.32              let val tn = find_tname (hd (map_filter I (flat varss))) Bi
    1.33                  val thy = Thm.theory_of_thm state
    1.34 -            in (#induction (the_datatype thy tn), "Induction rule for type " ^ tn) 
    1.35 +            in (#induction (the_datatype thy tn), "Induction rule for type " ^ tn)
    1.36              end
    1.37      val concls = HOLogic.dest_concls (Thm.concl_of rule);
    1.38      val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
    1.39 @@ -423,7 +423,7 @@
    1.40  
    1.41  fun add_case_tr' case_names thy =
    1.42    Theory.add_advanced_trfuns ([], [],
    1.43 -    map (fn case_name => 
    1.44 +    map (fn case_name =>
    1.45        let val case_name' = Sign.const_syntax_name thy case_name
    1.46        in (case_name', DatatypeCase.case_tr' datatype_of_case case_name')
    1.47        end) case_names, []) thy;
    1.48 @@ -519,9 +519,8 @@
    1.49  val specify_consts = gen_specify_consts Sign.add_consts_i;
    1.50  val specify_consts_authentic = gen_specify_consts Sign.add_consts_authentic;
    1.51  
    1.52 -structure DatatypeInterpretator = TheoryInterpretatorFun(struct type T = string list; val eq = op = end);
    1.53 -
    1.54 -fun add_interpretator interpretator = DatatypeInterpretator.add_interpretator (fold interpretator);
    1.55 +structure DatatypeInterpretation = InterpretationFun(type T = string list val eq = op =);
    1.56 +val interpretation = DatatypeInterpretation.interpretation;
    1.57  
    1.58  fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
    1.59      case_names_induct case_names_exhausts thy =
    1.60 @@ -641,7 +640,7 @@
    1.61        |> Theory.parent_path
    1.62        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
    1.63        |> snd
    1.64 -      |> DatatypeInterpretator.add_those [map fst dt_infos];
    1.65 +      |> DatatypeInterpretation.data (map fst dt_infos);
    1.66    in
    1.67      ({distinct = distinct,
    1.68        inject = inject,
    1.69 @@ -698,7 +697,7 @@
    1.70        |> add_cases_induct dt_infos induct
    1.71        |> Theory.parent_path
    1.72        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
    1.73 -      |> DatatypeInterpretator.add_those [map fst dt_infos];
    1.74 +      |> DatatypeInterpretation.data (map fst dt_infos);
    1.75    in
    1.76      ({distinct = distinct,
    1.77        inject = inject,
    1.78 @@ -799,7 +798,7 @@
    1.79        |> Theory.parent_path
    1.80        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
    1.81        |> snd
    1.82 -      |> DatatypeInterpretator.add_those [map fst dt_infos];
    1.83 +      |> DatatypeInterpretation.data (map fst dt_infos);
    1.84    in
    1.85      ({distinct = distinct,
    1.86        inject = inject,
    1.87 @@ -902,7 +901,7 @@
    1.88    Method.add_methods tactic_emulations #>
    1.89    simproc_setup #>
    1.90    trfun_setup #>
    1.91 -  DatatypeInterpretator.init;
    1.92 +  DatatypeInterpretation.init;
    1.93  
    1.94  
    1.95  (* outer syntax *)