read_typ/term: context_of;
authorwenzelm
Tue Sep 07 16:57:15 1999 +0200 (1999-09-07 ago)
changeset 7503e8be98558eb8
parent 7502 257dd7777676
child 7504 0fec51813079
read_typ/term: context_of;
src/Pure/Isar/isar_cmd.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Sep 07 16:56:47 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Sep 07 16:57:15 1999 +0200
     1.3 @@ -150,24 +150,16 @@
     1.4    let val st = Toplevel.node_case Proof.init_state Proof.enter_forward state
     1.5    in Pretty.writeln (Proof.pretty_thms (IsarThy.get_thmss args st)) end);
     1.6  
     1.7 -
     1.8 -fun read_typ thy = Sign.read_typ (Theory.sign_of thy, K None);
     1.9 -
    1.10 -fun read_term T thy s =
    1.11 -  Thm.term_of (#1 (Thm.read_def_cterm (Theory.sign_of thy, K None, K None) [] true (s, T)));
    1.12 -
    1.13 -
    1.14  fun print_type s = Toplevel.keep (fn state =>
    1.15    let
    1.16      val sign = Toplevel.sign_of state;
    1.17 -    val T = Toplevel.node_case read_typ (ProofContext.read_typ o Proof.context_of) state s;
    1.18 +    val T = ProofContext.read_typ (Toplevel.context_of state) s;
    1.19    in Pretty.writeln (Pretty.quote (Sign.pretty_typ sign T)) end);
    1.20  
    1.21  fun print_term s = Toplevel.keep (fn state =>
    1.22    let
    1.23      val sign = Toplevel.sign_of state;
    1.24 -    val t = Toplevel.node_case (read_term (TVar (("'z", 0), logicS)))
    1.25 -      (ProofContext.read_term o Proof.context_of) state s;
    1.26 +    val t = ProofContext.read_term (Toplevel.context_of state) s;
    1.27      val T = Term.type_of t;
    1.28    in
    1.29      Pretty.writeln (Pretty.block [Pretty.quote (Sign.pretty_term sign t), Pretty.fbrk,
    1.30 @@ -177,8 +169,7 @@
    1.31  fun print_prop s = Toplevel.keep (fn state =>
    1.32    let
    1.33      val sign = Toplevel.sign_of state;
    1.34 -    val prop =
    1.35 -      Toplevel.node_case (read_term propT) (ProofContext.read_prop o Proof.context_of) state s;
    1.36 +    val prop = ProofContext.read_prop (Toplevel.context_of state) s;
    1.37    in Pretty.writeln (Pretty.quote (Sign.pretty_term sign prop)) end);
    1.38  
    1.39