--- a/src/Pure/Tools/find_consts.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Tools/find_consts.ML Sat Apr 16 15:47:52 2011 +0200
@@ -71,7 +71,7 @@
let
val start = Timing.start ();
- val thy = ProofContext.theory_of ctxt;
+ val thy = Proof_Context.theory_of ctxt;
val low_ranking = 10000;
fun user_visible consts (nm, _) =
@@ -82,7 +82,7 @@
val raw_T = Syntax.parse_typ ctxt crit;
val t =
Syntax.check_term
- (ProofContext.set_mode ProofContext.mode_pattern ctxt)
+ (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
(Term.dummy_pattern raw_T);
in Term.type_of t end;