# HG changeset patch
# User blanchet
# Date 1409581067 -7200
# Node ID bfde04fc519027f7bcc38a60f96feb148fc080f3
# Parent  4e5a43b0e7dd3cce59123b38ecbde4c73f2a2e6c
made transfer functions slightly more general

diff -r 4e5a43b0e7dd -r bfde04fc5190 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 01 16:17:47 2014 +0200
@@ -24,7 +24,7 @@
     (thm list * thm * Token.src list) * (thm list list * Token.src list)
 
   val morph_lfp_sugar_thms: morphism -> lfp_sugar_thms -> lfp_sugar_thms
-  val transfer_lfp_sugar_thms: Proof.context -> lfp_sugar_thms -> lfp_sugar_thms
+  val transfer_lfp_sugar_thms: theory -> lfp_sugar_thms -> lfp_sugar_thms
 
   type gfp_sugar_thms =
     ((thm list * thm) list * (Token.src list * Token.src list))
@@ -34,7 +34,7 @@
     * (thm list list list * Token.src list)
 
   val morph_gfp_sugar_thms: morphism -> gfp_sugar_thms -> gfp_sugar_thms
-  val transfer_gfp_sugar_thms: Proof.context -> gfp_sugar_thms -> gfp_sugar_thms
+  val transfer_gfp_sugar_thms: theory -> gfp_sugar_thms -> gfp_sugar_thms
 
   val mk_co_recs_prelims: BNF_Util.fp_kind -> typ list list list -> typ list -> typ list ->
      typ list -> typ list -> int list -> int list list -> term list -> Proof.context ->
@@ -143,10 +143,11 @@
 
 fun fp_sugar_of ctxt =
   Symtab.lookup (Data.get (Context.Proof ctxt))
-  #> Option.map (transfer_fp_sugar ctxt);
+  #> Option.map (transfer_fp_sugar (Proof_Context.theory_of ctxt));
 
 fun fp_sugars_of ctxt =
-  Symtab.fold (cons o transfer_fp_sugar ctxt o snd) (Data.get (Context.Proof ctxt)) [];
+  Symtab.fold (cons o transfer_fp_sugar (Proof_Context.theory_of ctxt) o snd)
+    (Data.get (Context.Proof ctxt)) [];
 
 fun co_induct_of (i :: _) = i;
 fun strong_co_induct_of [_, s] = s;
@@ -308,8 +309,7 @@
    (map (map (Morphism.thm phi)) recss, rec_attrs))
   : lfp_sugar_thms;
 
-val transfer_lfp_sugar_thms =
-  morph_lfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
+val transfer_lfp_sugar_thms = morph_lfp_sugar_thms o Morphism.transfer_morphism;
 
 type gfp_sugar_thms =
   ((thm list * thm) list * (Token.src list * Token.src list))
@@ -328,8 +328,7 @@
    (map (map (Morphism.thm phi)) corec_disc_iffss, corec_disc_iff_attrs),
    (map (map (map (Morphism.thm phi))) corec_selsss, corec_sel_attrs)) : gfp_sugar_thms;
 
-val transfer_gfp_sugar_thms =
-  morph_gfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
+val transfer_gfp_sugar_thms = morph_gfp_sugar_thms o Morphism.transfer_morphism;
 
 fun mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss ctor_rec_fun_Ts lthy =
   let
diff -r 4e5a43b0e7dd -r bfde04fc5190 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Sep 01 16:17:47 2014 +0200
@@ -50,12 +50,11 @@
    (Option.map (morph_lfp_sugar_thms phi) lfp_sugar_thms_opt,
     Option.map (morph_gfp_sugar_thms phi) gfp_sugar_thms_opt));
 
-val transfer_n2m_sugar =
-  morph_n2m_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
+val transfer_n2m_sugar = morph_n2m_sugar o Morphism.transfer_morphism;
 
 fun n2m_sugar_of ctxt =
   Typtab.lookup (Data.get (Context.Proof ctxt))
-  #> Option.map (transfer_n2m_sugar ctxt);
+  #> Option.map (transfer_n2m_sugar (Proof_Context.theory_of ctxt));
 
 fun register_n2m_sugar key n2m_sugar =
   Local_Theory.declaration {syntax = false, pervasive = false}
diff -r 4e5a43b0e7dd -r bfde04fc5190 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Sep 01 16:17:47 2014 +0200
@@ -56,7 +56,7 @@
      rel_distincts: thm list};
 
   val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
-  val transfer_fp_sugar: Proof.context -> fp_sugar -> fp_sugar
+  val transfer_fp_sugar: theory -> fp_sugar -> fp_sugar
 
   val time: Proof.context -> Timer.real_timer -> string -> Timer.real_timer
 
@@ -314,7 +314,7 @@
    rel_injects = map (Morphism.thm phi) rel_injects,
    rel_distincts = map (Morphism.thm phi) rel_distincts};
 
-val transfer_fp_sugar = morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
+val transfer_fp_sugar = morph_fp_sugar o Morphism.transfer_morphism;
 
 fun time ctxt timer msg = (if Config.get ctxt bnf_timing
   then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^
diff -r 4e5a43b0e7dd -r bfde04fc5190 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Sep 01 16:17:47 2014 +0200
@@ -36,7 +36,7 @@
      case_eq_ifs: thm list};
 
   val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar
-  val transfer_ctr_sugar: Proof.context -> 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_sugars_of: Proof.context -> ctr_sugar list
   val ctr_sugar_of_case: Proof.context -> string -> ctr_sugar option
@@ -138,8 +138,7 @@
    split_sel_asms = map (Morphism.thm phi) split_sel_asms,
    case_eq_ifs = map (Morphism.thm phi) case_eq_ifs};
 
-val transfer_ctr_sugar =
-  morph_ctr_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
+val transfer_ctr_sugar = morph_ctr_sugar o Morphism.transfer_morphism;
 
 structure Data = Generic_Data
 (
@@ -151,10 +150,11 @@
 
 fun ctr_sugar_of ctxt =
   Symtab.lookup (Data.get (Context.Proof ctxt))
-  #> Option.map (transfer_ctr_sugar ctxt);
+  #> Option.map (transfer_ctr_sugar (Proof_Context.theory_of ctxt));
 
 fun ctr_sugars_of ctxt =
-  Symtab.fold (cons o transfer_ctr_sugar ctxt o snd) (Data.get (Context.Proof 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 ctxt s =
   find_first (fn {casex = Const (s', _), ...} => s' = s | _ => false) (ctr_sugars_of ctxt);