src/HOL/Tools/inductive_set.ML

--- a/src/HOL/Tools/inductive_set.ML	Sat Apr 16 15:47:52 2011 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Sat Apr 16 16:15:37 2011 +0200
@@ -410,7 +410,7 @@
     {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
     cs intros monos params cnames_syn lthy =
   let
-    val thy = ProofContext.theory_of lthy;
+    val thy = Proof_Context.theory_of lthy;
     val {set_arities, pred_arities, to_pred_simps, ...} =
       PredSetConvData.get (Context.Proof lthy);
     fun infer (Abs (_, _, t)) = infer t