--- a/src/Pure/Isar/args.ML Wed Nov 07 18:19:04 2007 +0100
+++ b/src/Pure/Isar/args.ML Wed Nov 07 22:20:09 2007 +0100
@@ -322,7 +322,7 @@
(* terms and types *)
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 typ = Scan.peek (named_typ o Syntax.read_typ 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 Syntax.read_prop o Context.proof_of);
--- a/src/Pure/Isar/isar_cmd.ML Wed Nov 07 18:19:04 2007 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Wed Nov 07 22:20:09 2007 +0100
@@ -578,7 +578,7 @@
fun string_of_type state s =
let
val ctxt = Proof.context_of state;
- val T = ProofContext.read_typ ctxt s;
+ val T = Syntax.read_typ ctxt s;
in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end;
fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>