src/HOL/Tools/BNF/bnf_def.ML

   val morph_bnf: morphism -> bnf -> bnf
   val morph_bnf_defs: morphism -> bnf -> bnf
   val transfer_bnf: theory -> bnf -> bnf
   val bnf_of: Proof.context -> string -> bnf option
   val bnf_of_global: theory -> string -> bnf option
-  val bnf_interpretation: string -> (bnf -> theory -> theory) ->
-    (bnf -> local_theory -> local_theory) -> theory -> theory
+  val bnf_interpretation: string -> (bnf -> local_theory -> local_theory) -> theory -> theory
   val interpret_bnf: (string -> bool) -> bnf -> local_theory -> local_theory
   val register_bnf_raw: string -> bnf -> local_theory -> local_theory
   val register_bnf: (string -> bool) -> string -> bnf -> local_theory -> local_theory
 
   val name_of_bnf: bnf -> binding

       no_reflexive (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @ [bnf_rel_def]);
   in
     (key, goals, wit_goalss, after_qed, lthy, one_step_defs)
   end;
 
-structure BNF_Interpretation = Local_Interpretation
-(
-  type T = bnf;
-  val eq: T * T -> bool = op = o pairself T_of_bnf;
-);
-
-fun with_transfer_bnf g bnf thy = g (transfer_bnf thy bnf) thy;
-
-fun bnf_interpretation name =
-  BNF_Interpretation.interpretation name o with_transfer_bnf;
-
-val interpret_bnf = BNF_Interpretation.data;
+structure BNF_Plugin = Plugin(type T = bnf);
+
+fun bnf_interpretation name f =
+  BNF_Plugin.interpretation name
+    (fn bnf => fn lthy => f (transfer_bnf (Proof_Context.theory_of lthy) bnf) lthy);
+
+val interpret_bnf = BNF_Plugin.data;
 
 fun register_bnf_raw key bnf =
   Local_Theory.declaration {syntax = false, pervasive = true}
     (fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf)));
 

         unfold_thms_tac ctxt one_step_defs THEN tac ctxt) tacs)
     |> (fn thms => after_qed mk_wit_thms (map single thms) lthy)
   end) o prepare_def const_policy fact_policy internal qualify (K I) (K I) Ds map_b rel_b set_bs
     raw_csts;
 
-fun bnf_cmd (raw_csts, plugins) =
+fun bnf_cmd (raw_csts, raw_plugins) =
   (fn (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, defs) =>
   let
+    val plugins = raw_plugins lthy;
     val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
     fun mk_triv_wit_thms tac set_maps =
       Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
         (fn {context = ctxt, prems = _} => TRYALL Goal.conjunction_tac THEN tac ctxt set_maps)
         |> Conjunction.elim_balanced (length wit_goals)

        (Parse.reserved "bd" -- @{keyword ":"}) -- Parse.term --
        Scan.optional ((Parse.reserved "wits" -- @{keyword ":"}) |--
          Scan.repeat1 (Scan.unless (Parse.reserved "rel" ||
            Parse.reserved "plugins") Parse.term)) [] --
        Scan.option ((Parse.reserved "rel" -- @{keyword ":"}) |-- Parse.term) --
-       Scan.optional parse_plugins (K true)
+       Scan.optional Plugin_Name.parse_filter (K (K true))
        >> bnf_cmd);
 
-val _ = Context.>> (Context.map_theory BNF_Interpretation.init);
-
 end;