tuned signature;
authorwenzelm
Mon Oct 13 21:46:41 2014 +0200 (2014-10-13 ago)
changeset 586669e3426766267
parent 58665 50b229a5a097
child 58667 d2a7b443ceb2
tuned signature;
src/HOL/Tools/Old_Datatype/old_datatype_data.ML
src/Pure/Isar/code.ML
src/Pure/Tools/plugin.ML
     1.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Mon Oct 13 21:41:29 2014 +0200
     1.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Mon Oct 13 21:46:41 2014 +0200
     1.3 @@ -251,8 +251,7 @@
     1.4          |> f config type_names
     1.5          |> Sign.restore_naming thy));
     1.6  
     1.7 -val interpretation_data =
     1.8 -  Named_Target.theory_map o Old_Datatype_Plugin.data Plugin_Name.default_filter;
     1.9 +val interpretation_data = Named_Target.theory_map o Old_Datatype_Plugin.data_default;
    1.10  
    1.11  
    1.12  open Old_Datatype_Aux;
     2.1 --- a/src/Pure/Isar/code.ML	Mon Oct 13 21:41:29 2014 +0200
     2.2 +++ b/src/Pure/Isar/code.ML	Mon Oct 13 21:46:41 2014 +0200
     2.3 @@ -1257,7 +1257,7 @@
     2.4    in
     2.5      thy
     2.6      |> register_type (tyco, (vs, Constructors (cos, [])))
     2.7 -    |> Named_Target.theory_map (Datatype_Plugin.data Plugin_Name.default_filter tyco)
     2.8 +    |> Named_Target.theory_map (Datatype_Plugin.data_default tyco)
     2.9    end;
    2.10  
    2.11  fun add_datatype_cmd raw_constrs thy =
    2.12 @@ -1281,7 +1281,7 @@
    2.13      |> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
    2.14      |> change_fun_spec rep
    2.15        (K (Proj (Logic.varify_types_global (mk_proj tyco vs ty abs rep), tyco)))
    2.16 -    |> Named_Target.theory_map (Abstype_Plugin.data Plugin_Name.default_filter tyco)
    2.17 +    |> Named_Target.theory_map (Abstype_Plugin.data_default tyco)
    2.18    end;
    2.19  
    2.20  
     3.1 --- a/src/Pure/Tools/plugin.ML	Mon Oct 13 21:41:29 2014 +0200
     3.2 +++ b/src/Pure/Tools/plugin.ML	Mon Oct 13 21:46:41 2014 +0200
     3.3 @@ -97,6 +97,7 @@
     3.4  sig
     3.5    type T
     3.6    val data: Plugin_Name.filter -> T -> local_theory -> local_theory
     3.7 +  val data_default: T -> local_theory -> local_theory
     3.8    val interpretation: string -> (T -> local_theory -> local_theory) -> theory -> theory
     3.9  end;
    3.10  
    3.11 @@ -178,6 +179,8 @@
    3.12      Plugin_Data.map (apfst (cons (mk_data filter (Sign.naming_of thy) x))) thy)
    3.13    #> consolidate;
    3.14  
    3.15 +val data_default = data Plugin_Name.default_filter;
    3.16 +
    3.17  fun interpretation name f =
    3.18    Plugin_Data.map (apsnd (cons (mk_interp name f, [])))
    3.19    #> perhaps consolidate';