# HG changeset patch
# User wenzelm
# Date 936716235 -7200
# Node ID e8be98558eb810b575e78ed7db535fe8b57c94c1
# Parent  257dd777767649cc488c1591caffc0a3022bb595
read_typ/term: context_of;

diff -r 257dd7777676 -r e8be98558eb8 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Sep 07 16:56:47 1999 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Sep 07 16:57:15 1999 +0200
@@ -150,24 +150,16 @@
   let val st = Toplevel.node_case Proof.init_state Proof.enter_forward state
   in Pretty.writeln (Proof.pretty_thms (IsarThy.get_thmss args st)) end);
 
-
-fun read_typ thy = Sign.read_typ (Theory.sign_of thy, K None);
-
-fun read_term T thy s =
-  Thm.term_of (#1 (Thm.read_def_cterm (Theory.sign_of thy, K None, K None) [] true (s, T)));
-
-
 fun print_type s = Toplevel.keep (fn state =>
   let
     val sign = Toplevel.sign_of state;
-    val T = Toplevel.node_case read_typ (ProofContext.read_typ o Proof.context_of) state s;
+    val T = ProofContext.read_typ (Toplevel.context_of state) s;
   in Pretty.writeln (Pretty.quote (Sign.pretty_typ sign T)) end);
 
 fun print_term s = Toplevel.keep (fn state =>
   let
     val sign = Toplevel.sign_of state;
-    val t = Toplevel.node_case (read_term (TVar (("'z", 0), logicS)))
-      (ProofContext.read_term o Proof.context_of) state s;
+    val t = ProofContext.read_term (Toplevel.context_of state) s;
     val T = Term.type_of t;
   in
     Pretty.writeln (Pretty.block [Pretty.quote (Sign.pretty_term sign t), Pretty.fbrk,
@@ -177,8 +169,7 @@
 fun print_prop s = Toplevel.keep (fn state =>
   let
     val sign = Toplevel.sign_of state;
-    val prop =
-      Toplevel.node_case (read_term propT) (ProofContext.read_prop o Proof.context_of) state s;
+    val prop = ProofContext.read_prop (Toplevel.context_of state) s;
   in Pretty.writeln (Pretty.quote (Sign.pretty_term sign prop)) end);