--- 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