tuned;

--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Fri Mar 06 23:57:01 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Sat Mar 07 00:45:15 2015 +0100
@@ -346,12 +346,12 @@
 
 fun get_all thy prefs =
   let
-    val lthy = Proof_Context.init_global thy;
+    val ctxt = Proof_Context.init_global thy;
     val old_info_tab = Old_Datatype_Data.get_all thy;
     val new_T_names = BNF_FP_Def_Sugar.fp_sugars_of_global thy
       |> map_filter (try (fn {T = Type (s, _), fp_res_index = 0, ...} => s));
     val new_infos =
-      maps (infos_of_new_datatype_mutual_cluster lthy (insert (op =) Keep_Nesting prefs))
+      maps (infos_of_new_datatype_mutual_cluster ctxt (insert (op =) Keep_Nesting prefs))
         new_T_names;
   in
     fold (if member (op =) prefs Keep_Nesting then Symtab.update else Symtab.default) new_infos
@@ -366,8 +366,8 @@
   end;
 
 fun get_info_of_new_datatype prefs thy T_name =
-  let val lthy = Proof_Context.init_global thy in
-    AList.lookup (op =) (infos_of_new_datatype_mutual_cluster lthy prefs T_name) T_name
+  let val ctxt = Proof_Context.init_global thy in
+    AList.lookup (op =) (infos_of_new_datatype_mutual_cluster ctxt prefs T_name) T_name
   end;
 
 fun get_info thy prefs =

--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Fri Mar 06 23:57:01 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Sat Mar 07 00:45:15 2015 +0100
@@ -212,8 +212,8 @@
           val (thm, lthy') = lthy
             |> Local_Theory.define ((Binding.name c, NoSyn), ((def_b, []), rhs))
             |-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm);
-          val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');
-          val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm;
+          val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy');
+          val thm' = singleton (Proof_Context.export lthy' thy_ctxt) thm;
         in (thm', lthy') end;
 
       val (overloaded_size_defs, lthy2) = lthy1

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Fri Mar 06 23:57:01 2015 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Sat Mar 07 00:45:15 2015 +0100
@@ -87,8 +87,8 @@
           |> Syntax.check_term lthy;
         val ((_, (_, raw_def)), lthy') =
           Specification.definition (NONE, (Attrib.empty_binding, spec)) lthy;
-        val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy); (* FIXME? *)
-        val def = singleton (Proof_Context.export lthy' ctxt_thy) raw_def;
+        val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy); (* FIXME? *)
+        val def = singleton (Proof_Context.export lthy' thy_ctxt) raw_def;
       in
         (def, lthy')
       end;