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