# HG changeset patch
# User wenzelm
# Date 1194470409 -3600
# Node ID 73072178e0cec0dfa59fec08d5c0fff5657b5d63
# Parent  15bf0f47a87d8fc2115707b004fff6ae484fa839
Syntax.read_typ;

diff -r 15bf0f47a87d -r 73072178e0ce src/Pure/Isar/args.ML
--- 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);
diff -r 15bf0f47a87d -r 73072178e0ce src/Pure/Isar/isar_cmd.ML
--- 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 =>