--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Oct 13 17:04:25 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Oct 13 18:45:48 2014 +0200
@@ -7,7 +7,6 @@
signature BNF_LFP_SIZE =
sig
- val size_plugin: string
val register_size: string -> string -> thm list -> thm list -> local_theory -> local_theory
val register_size_global: string -> string -> thm list -> thm list -> theory -> theory
val size_of: Proof.context -> string -> (string * (thm list * thm list)) option
@@ -22,8 +21,6 @@
open BNF_Def
open BNF_FP_Def_Sugar
-val size_plugin = "size";
-
val size_N = "size_";
val rec_o_mapN = "rec_o_map";
@@ -396,7 +393,7 @@
end
| generate_datatype_size _ lthy = lthy;
-val _ = Theory.setup (fp_sugars_interpretation size_plugin
- (map_local_theory o generate_datatype_size) generate_datatype_size);
+val size_plugin = Plugin_Name.declare_setup @{binding size};
+val _ = Theory.setup (fp_sugars_interpretation size_plugin generate_datatype_size);
end;