src/HOL/Tools/recdef.ML

--- a/src/HOL/Tools/recdef.ML	Sat Apr 16 15:47:52 2011 +0200
+++ b/src/HOL/Tools/recdef.ML	Sat Apr 16 16:15:37 2011 +0200
@@ -160,7 +160,7 @@
 
 fun prepare_hints thy opt_src =
   let
-    val ctxt0 = ProofContext.init_global thy;
+    val ctxt0 = Proof_Context.init_global thy;
     val ctxt =
       (case opt_src of
         NONE => ctxt0
@@ -172,7 +172,7 @@
 
 fun prepare_hints_i thy () =
   let
-    val ctxt0 = ProofContext.init_global thy;
+    val ctxt0 = Proof_Context.init_global thy;
     val {simps, congs, wfs} = get_global_hints thy;
   in (claset_of ctxt0, simpset_of ctxt0 addsimps simps, rev (map snd congs), wfs) end;
 
@@ -234,7 +234,7 @@
     val _ = requires_recdef thy;
     val _ = writeln ("Deferred recursive function " ^ quote name ^ " ...");
 
-    val congs = eval_thms (ProofContext.init_global thy) raw_congs;
+    val congs = eval_thms (Proof_Context.init_global thy) raw_congs;
     val (thy2, induct_rules) = tfl_fn thy congs name eqs;
     val ([induct_rules'], thy3) =
       thy2
@@ -252,7 +252,7 @@
 
 fun gen_recdef_tc prep_att prep_name (bname, raw_atts) raw_name opt_i int lthy =
   let
-    val thy = ProofContext.theory_of lthy;
+    val thy = Proof_Context.theory_of lthy;
     val name = prep_name thy raw_name;
     val atts = map (prep_att thy) raw_atts;
     val tcs =