src/HOL/Tools/inductive.ML

       else
         map_index (fn (i, (name_mx, c)) =>
           let
             val Ts = arg_types_of (length params) c;
             val xs =
-              map Free (Variable.variant_frees lthy intr_ts (mk_names "x" (length Ts) ~~ Ts));
+              map Free (Variable.variant_frees lthy' intr_ts (mk_names "x" (length Ts) ~~ Ts));
           in
             (name_mx, (apfst Binding.concealed Attrib.empty_binding, fold_rev lambda (params @ xs)
               (list_comb (rec_const, params @ make_bool_args' bs i @
                 make_args argTs (xs ~~ Ts)))))
           end) (cnames_syn ~~ cs);
     val (consts_defs, lthy'') = lthy'
       |> fold_map Local_Theory.define specs;
     val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
 
-    val (_, lthy''') = Variable.add_fixes (map (fst o dest_Free) params) lthy'';
-    val mono = prove_mono quiet_mode skip_mono predT fp_fun monos lthy''';
-    val (_, lthy'''') =
-      Local_Theory.note (apfst Binding.concealed Attrib.empty_binding,
-        Proof_Context.export lthy''' lthy'' [mono]) lthy'';
-
-  in (lthy'''', lthy''', rec_name, mono, fp_def', map (#2 o #2) consts_defs,
-    list_comb (rec_const, params), preds, argTs, bs, xs)
+    val (_, ctxt'') = Variable.add_fixes (map (fst o dest_Free) params) lthy'';
+    val mono = prove_mono quiet_mode skip_mono predT fp_fun monos ctxt'';
+    val (_, lthy''') = lthy''
+      |> Local_Theory.note (apfst Binding.concealed Attrib.empty_binding,
+        Proof_Context.export ctxt'' lthy'' [mono]);
+  in
+    (lthy''', Proof_Context.transfer (Proof_Context.theory_of lthy''') ctxt'',
+      rec_name, mono, fp_def', map (#2 o #2) consts_defs,
+      list_comb (rec_const, params), preds, argTs, bs, xs)
   end;
 
 fun declare_rules rec_binding coind no_ind cnames
     preds intrs intr_bindings intr_atts elims eqs raw_induct lthy =
   let