1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Sep 18 07:36:38 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Sep 18 07:46:00 2007 +0200
     1.3 @@ -69,6 +69,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 print_datatypes : theory -> unit
     1.9    val make_case :  Proof.context -> bool -> string list -> term ->
    1.10      (term * term) list -> term * (term * (int * bool)) list
    1.11 @@ -521,6 +522,10 @@
    1.12  val specify_consts = gen_specify_consts Sign.add_consts_i;
    1.13  val specify_consts_authentic = gen_specify_consts Sign.add_consts_authentic;
    1.14  
    1.15 +structure DatatypeInterpretator = TheoryInterpretatorFun(struct type T = string; val eq = op = end);
    1.16 +
    1.17 +fun add_interpretator interpretator = DatatypeInterpretator.add_interpretator interpretator;
    1.18 +
    1.19  fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
    1.20      case_names_induct case_names_exhausts thy =
    1.21    let
    1.22 @@ -666,7 +671,7 @@
    1.23        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
    1.24        |> snd
    1.25        |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
    1.26 -      |> DatatypeHooks.all (map fst dt_infos);
    1.27 +      |> DatatypeInterpretator.add_those (map fst dt_infos);
    1.28    in
    1.29      ({distinct = distinct,
    1.30        inject = inject,
    1.31 @@ -726,7 +731,7 @@
    1.32        |> Theory.parent_path
    1.33        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
    1.34        |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
    1.35 -      |> DatatypeHooks.all (map fst dt_infos);
    1.36 +      |> DatatypeInterpretator.add_those (map fst dt_infos);
    1.37    in
    1.38      ({distinct = distinct,
    1.39        inject = inject,
    1.40 @@ -831,7 +836,7 @@
    1.41        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
    1.42        |> snd
    1.43        |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
    1.44 -      |> DatatypeHooks.all (map fst dt_infos);
    1.45 +      |> DatatypeInterpretator.add_those (map fst dt_infos);
    1.46    in
    1.47      ({distinct = distinct,
    1.48        inject = inject,
    1.49 @@ -934,7 +939,8 @@
    1.50    DatatypeProp.distinctness_limit_setup #>
    1.51    Method.add_methods tactic_emulations #>
    1.52    simproc_setup #>
    1.53 -  trfun_setup;
    1.54 +  trfun_setup #>
    1.55 +  DatatypeInterpretator.init;
    1.56  
    1.57  
    1.58  (* outer syntax *)