--- a/src/HOL/Tools/BNF/bnf_def.ML Mon Sep 01 16:17:47 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Mon Sep 01 16:17:47 2014 +0200
@@ -15,6 +15,7 @@
val morph_bnf: morphism -> bnf -> bnf
val morph_bnf_defs: morphism -> bnf -> bnf
val bnf_of: Proof.context -> string -> bnf option
+ val bnf_of_global: theory -> string -> bnf option
val bnf_interpretation: (bnf -> theory -> theory) -> theory -> theory
val register_bnf: string -> bnf -> local_theory -> local_theory
@@ -522,9 +523,12 @@
fun merge data : T = Symtab.merge (K true) data;
);
-fun bnf_of ctxt =
- Symtab.lookup (Data.get (Context.Proof ctxt))
- #> Option.map (morph_bnf (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)));
+fun bnf_of_generic context =
+ Option.map (morph_bnf (Morphism.transfer_morphism (Context.theory_of context)))
+ o Symtab.lookup (Data.get context);
+
+val bnf_of = bnf_of_generic o Context.Proof;
+val bnf_of_global = bnf_of_generic o Context.Theory;
(* Utilities *)