diff -r 6292f1f5ffae -r 30687c3f2b10 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Tue Mar 31 16:47:12 2015 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Tue Mar 31 17:34:52 2015 +0200
@@ -488,13 +488,13 @@
 
     (* define inductive sets using previously defined predicates *)
     val (defs, lthy2) = lthy1
-      |> Local_Theory.concealed  (* FIXME ?? *)
+      |> Proof_Context.concealed  (* FIXME ?? *)
       |> fold_map Local_Theory.define
         (map (fn (((c, syn), (fs, U, _)), p) => ((c, syn), ((Thm.def_binding c, []),
            fold_rev lambda params (HOLogic.Collect_const U $
              HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
            (cnames_syn ~~ cs_info ~~ preds))
-      ||> Local_Theory.restore_naming lthy1;
+      ||> Proof_Context.restore_naming lthy1;
 
     (* prove theorems for converting predicate to set notation *)
     val lthy3 = fold