--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Mon Oct 13 17:04:25 2014 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Mon Oct 13 18:45:48 2014 +0200
@@ -6,7 +6,6 @@
signature TRANSFER_BNF =
sig
- val transfer_plugin: string
val base_name_of_bnf: BNF_Def.bnf -> binding
val type_name_of_bnf: BNF_Def.bnf -> string
val lookup_defined_pred_data: Proof.context -> string -> Transfer.pred_data
@@ -21,8 +20,6 @@
open BNF_FP_Util
open BNF_FP_Def_Sugar
-val transfer_plugin = "transfer"
-
(* util functions *)
fun base_name_of_bnf bnf = Binding.name (Binding.name_of (name_of_bnf bnf))
@@ -282,6 +279,8 @@
(* BNF interpretation *)
+val transfer_plugin = Plugin_Name.declare_setup @{binding transfer}
+
fun transfer_bnf_interpretation bnf lthy =
let
val dead = dead_of_bnf bnf
@@ -294,9 +293,9 @@
|> predicator bnf
end
-val _ = Theory.setup (bnf_interpretation transfer_plugin
- (bnf_only_type_ctr (BNF_Util.map_local_theory o transfer_bnf_interpretation))
- (bnf_only_type_ctr transfer_bnf_interpretation))
+val _ =
+ Theory.setup
+ (bnf_interpretation transfer_plugin (bnf_only_type_ctr transfer_bnf_interpretation))
(* simplification rules for the predicator *)
@@ -370,8 +369,8 @@
snd (Local_Theory.note ((pred_inject_thm_name, simp_attrs), pred_injects) lthy)
end
-val _ = Theory.setup (fp_sugars_interpretation transfer_plugin
- (fp_sugar_only_type_ctr (map_local_theory o fold transfer_fp_sugars_interpretation))
- (fp_sugar_only_type_ctr (fold transfer_fp_sugars_interpretation)))
+val _ =
+ Theory.setup (fp_sugars_interpretation transfer_plugin
+ (fp_sugar_only_type_ctr (fold transfer_fp_sugars_interpretation)))
end