# HG changeset patch
# User blanchet
# Date 1389618662 -3600
# Node ID 38ea5ee18a060016a9a5962091fa46e9f2646d3a
# Parent  96dfb73bb11aa349dd1d02512d7f85f5e4b5bfd0
use the right context in 'unfold_thms id_def'

diff -r 96dfb73bb11a -r 38ea5ee18a06 src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Mon Jan 13 13:24:09 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Mon Jan 13 14:11:02 2014 +0100
@@ -374,14 +374,14 @@
     | NONE => [])
   | map_thms_of_typ _ _ = [];
 
-fun corec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy =
+fun corec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy0 =
   let
-    val thy = Proof_Context.theory_of lthy;
+    val thy = Proof_Context.theory_of lthy0;
 
     val ((missing_res_Ts, perm0_kks,
           fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...},
-            co_inducts = coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy') =
-      nested_to_mutual_fps Greatest_FP bs res_Ts get_indices callssss0 lthy;
+            co_inducts = coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
+      nested_to_mutual_fps Greatest_FP bs res_Ts get_indices callssss0 lthy0;
 
     val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
 
@@ -474,12 +474,13 @@
   in
     ((is_some gfp_sugar_thms, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
       co_induct_of coinduct_thms, strong_co_induct_of coinduct_thms, co_induct_of coinduct_thmss,
-      strong_co_induct_of coinduct_thmss), lthy')
+      strong_co_induct_of coinduct_thmss), lthy)
   end;
 
 val undef_const = Const (@{const_name undefined}, dummyT);
 
 val abs_tuple = HOLogic.tupled_lambda o HOLogic.mk_tuple;
+
 fun abstract vs =
   let fun a n (t $ u) = a n t $ a n u
         | a n (Abs (v, T, b)) = Abs (v, T, a (n + 1) b)
diff -r 96dfb73bb11a -r 38ea5ee18a06 src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML	Mon Jan 13 13:24:09 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML	Mon Jan 13 14:11:02 2014 +0100
@@ -133,14 +133,14 @@
     massage_call
   end;
 
-fun rec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy =
+fun rec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy0 =
   let
-    val thy = Proof_Context.theory_of lthy;
+    val thy = Proof_Context.theory_of lthy0;
 
     val ((missing_arg_Ts, perm0_kks,
           fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = ctor_iters1 :: _, ...},
-            co_inducts = [induct_thm], ...} :: _, (lfp_sugar_thms, _)), lthy') =
-      nested_to_mutual_fps Least_FP bs arg_Ts get_indices callssss0 lthy;
+            co_inducts = [induct_thm], ...} :: _, (lfp_sugar_thms, _)), lthy) =
+      nested_to_mutual_fps Least_FP bs arg_Ts get_indices callssss0 lthy0;
 
     val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
 
@@ -214,8 +214,7 @@
        nested_map_comps = map map_comp_of_bnf nested_bnfs,
        ctr_specs = mk_ctr_specs index ctr_sugars iter_thmsss};
   in
-    ((is_some lfp_sugar_thms, map mk_spec fp_sugars, missing_arg_Ts, induct_thm, induct_thms),
-     lthy')
+    ((is_some lfp_sugar_thms, map mk_spec fp_sugars, missing_arg_Ts, induct_thm, induct_thms), lthy)
   end;
 
 val undef_const = Const (@{const_name undefined}, dummyT);