# 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 =>