# HG changeset patch
# User blanchet
# Date 1409581067 -7200
# Node ID 1a9ac371e5a086c3bf5f107e1cfe24a29f161194
# Parent  bfde04fc519027f7bcc38a60f96feb148fc080f3
added theory-based getters for convenience

diff -r bfde04fc5190 -r 1a9ac371e5a0 src/HOL/Tools/BNF/bnf_def.ML
--- 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 *)
diff -r bfde04fc5190 -r 1a9ac371e5a0 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 01 16:17:47 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 01 16:17:47 2014 +0200
@@ -9,7 +9,9 @@
 signature BNF_FP_DEF_SUGAR =
 sig
   val fp_sugar_of: Proof.context -> string -> BNF_FP_Util.fp_sugar option
+  val fp_sugar_of_global: theory -> string -> BNF_FP_Util.fp_sugar option
   val fp_sugars_of: Proof.context -> BNF_FP_Util.fp_sugar list
+  val fp_sugars_of_global: theory -> BNF_FP_Util.fp_sugar list
   val fp_sugar_interpretation: (BNF_FP_Util.fp_sugar list -> theory -> theory) -> theory -> theory
   val register_fp_sugars: BNF_FP_Util.fp_sugar list -> local_theory -> local_theory
 
@@ -141,13 +143,17 @@
 
 val name_of_set = name_of_const "set";
 
-fun fp_sugar_of ctxt =
-  Symtab.lookup (Data.get (Context.Proof ctxt))
-  #> Option.map (transfer_fp_sugar (Proof_Context.theory_of ctxt));
+fun fp_sugar_of_generic context =
+  Option.map (transfer_fp_sugar (Context.theory_of context)) o Symtab.lookup (Data.get context)
+
+fun fp_sugars_of_generic context =
+  Symtab.fold (cons o transfer_fp_sugar (Context.theory_of context) o snd) (Data.get context) [];
 
-fun fp_sugars_of ctxt =
-  Symtab.fold (cons o transfer_fp_sugar (Proof_Context.theory_of ctxt) o snd)
-    (Data.get (Context.Proof ctxt)) [];
+val fp_sugar_of = fp_sugar_of_generic o Context.Proof;
+val fp_sugar_of_global = fp_sugar_of_generic o Context.Theory;
+
+val fp_sugars_of = fp_sugars_of_generic o Context.Proof;
+val fp_sugars_of_global = fp_sugars_of_generic o Context.Theory;
 
 fun co_induct_of (i :: _) = i;
 fun strong_co_induct_of [_, s] = s;
diff -r bfde04fc5190 -r 1a9ac371e5a0 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Sep 01 16:17:47 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Sep 01 16:17:47 2014 +0200
@@ -38,8 +38,11 @@
   val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar
   val transfer_ctr_sugar: theory -> ctr_sugar -> ctr_sugar
   val ctr_sugar_of: Proof.context -> string -> ctr_sugar option
+  val ctr_sugar_of_global: theory -> string -> ctr_sugar option
   val ctr_sugars_of: Proof.context -> ctr_sugar list
+  val ctr_sugars_of_global: theory -> ctr_sugar list
   val ctr_sugar_of_case: Proof.context -> string -> ctr_sugar option
+  val ctr_sugar_of_case_global: theory -> string -> ctr_sugar option
   val ctr_sugar_interpretation: (ctr_sugar -> theory -> theory) -> theory -> theory
   val register_ctr_sugar: string -> ctr_sugar -> local_theory -> local_theory
   val default_register_ctr_sugar_global: string -> ctr_sugar -> theory -> theory
@@ -148,16 +151,24 @@
   fun merge data : T = Symtab.merge (K true) data;
 );
 
-fun ctr_sugar_of ctxt =
-  Symtab.lookup (Data.get (Context.Proof ctxt))
-  #> Option.map (transfer_ctr_sugar (Proof_Context.theory_of ctxt));
+fun ctr_sugar_of_generic context =
+  Option.map (transfer_ctr_sugar (Context.theory_of context)) o Symtab.lookup (Data.get context);
+
+fun ctr_sugars_of_generic context =
+  Symtab.fold (cons o transfer_ctr_sugar (Context.theory_of context) o snd) (Data.get context) [];
 
-fun ctr_sugars_of ctxt =
-  Symtab.fold (cons o transfer_ctr_sugar (Proof_Context.theory_of ctxt) o snd)
-    (Data.get (Context.Proof ctxt)) [];
+fun ctr_sugar_of_case_generic context s =
+  find_first (fn {casex = Const (s', _), ...} => s' = s | _ => false)
+    (ctr_sugars_of_generic context);
 
-fun ctr_sugar_of_case ctxt s =
-  find_first (fn {casex = Const (s', _), ...} => s' = s | _ => false) (ctr_sugars_of ctxt);
+val ctr_sugar_of = ctr_sugar_of_generic o Context.Proof;
+val ctr_sugar_of_global = ctr_sugar_of_generic o Context.Theory;
+
+val ctr_sugars_of = ctr_sugars_of_generic o Context.Proof;
+val ctr_sugars_of_global = ctr_sugars_of_generic o Context.Theory;
+
+val ctr_sugar_of_case = ctr_sugar_of_case_generic o Context.Proof;
+val ctr_sugar_of_case_global = ctr_sugar_of_case_generic o Context.Theory;
 
 structure Ctr_Sugar_Interpretation = Interpretation
 (