--- a/src/Pure/Isar/args.ML Sat Sep 01 01:22:11 2007 +0200
+++ b/src/Pure/Isar/args.ML Sat Sep 01 15:46:59 2007 +0200
@@ -323,9 +323,9 @@
val typ_abbrev = Scan.peek (named_typ o ProofContext.read_typ_abbrev o Context.proof_of);
val typ = Scan.peek (named_typ o ProofContext.read_typ o Context.proof_of);
-val term = Scan.peek (named_term o ProofContext.read_term o Context.proof_of);
+val term = Scan.peek (named_term o Syntax.read_term o Context.proof_of);
val term_abbrev = Scan.peek (named_term o ProofContext.read_term_abbrev o Context.proof_of);
-val prop = Scan.peek (named_term o ProofContext.read_prop o Context.proof_of);
+val prop = Scan.peek (named_term o Syntax.read_prop o Context.proof_of);
(* type and constant names *)