--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Sep 05 00:41:01 2014 +0200
@@ -7,7 +7,7 @@
signature BNF_LFP_SIZE =
sig
- val size_interpretation: string
+ 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,7 +22,7 @@
open BNF_Def
open BNF_FP_Def_Sugar
-val size_interpretation = "size"
+val size_plugin = "size"
val size_N = "size_"
@@ -376,7 +376,7 @@
end
| generate_datatype_size _ lthy = lthy;
-val _ = Theory.setup (fp_sugars_interpretation size_interpretation
+val _ = Theory.setup (fp_sugars_interpretation size_plugin
(map_local_theory o generate_datatype_size) generate_datatype_size);
end;