src/Pure/Isar/isar_cmd.ML
changeset 7012 ae9dac5af9d1
parent 6742 6b5cb872d997
child 7023 5d1eafaff50c
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Jul 15 17:53:28 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Jul 15 17:54:58 1999 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4    val print_methods: Toplevel.transition -> Toplevel.transition
     1.5    val print_binds: Toplevel.transition -> Toplevel.transition
     1.6    val print_lthms: Toplevel.transition -> Toplevel.transition
     1.7 -  val print_thms: xstring * Args.src list -> Toplevel.transition -> Toplevel.transition
     1.8 +  val print_thms: (string * Args.src list) list -> Toplevel.transition -> Toplevel.transition
     1.9    val print_prop: string -> Toplevel.transition -> Toplevel.transition
    1.10    val print_term: string -> Toplevel.transition -> Toplevel.transition
    1.11    val print_type: string -> Toplevel.transition -> Toplevel.transition
    1.12 @@ -125,26 +125,13 @@
    1.13  val print_lthms = Toplevel.keep (ProofContext.print_thms o Proof.context_of o Toplevel.proof_of);
    1.14  
    1.15  
    1.16 -(* print theorems *)
    1.17 -
    1.18 -fun global_attribs thy ths srcs =
    1.19 -  #2 (Thm.applys_attributes ((Theory.copy thy, ths), map (Attrib.global_attribute thy) srcs));
    1.20 -
    1.21 -fun local_attribs st ths srcs =
    1.22 -  #2 (Thm.applys_attributes ((Proof.context_of st, ths),
    1.23 -    map (Attrib.local_attribute (Proof.theory_of st)) srcs));
    1.24 +(* print theorems / types / terms / props *)
    1.25  
    1.26 -fun print_thms (name, srcs) = Toplevel.keep (fn state =>
    1.27 -  let
    1.28 -    val ths = map (Thm.transfer (Toplevel.theory_of state))
    1.29 -      (Toplevel.node_case PureThy.get_thms (ProofContext.get_thms o Proof.context_of)
    1.30 -        state name);
    1.31 -    val ths' = Toplevel.node_case global_attribs local_attribs state ths srcs;
    1.32 -  in Display.print_thms ths' end);
    1.33 +fun print_thms args = Toplevel.keep (fn state =>
    1.34 +  let val st = Toplevel.node_case Proof.init_state Proof.enter_forward state
    1.35 +  in Display.print_thms (IsarThy.get_thmss args st) end);
    1.36  
    1.37  
    1.38 -(* print types, terms and props *)
    1.39 -
    1.40  fun read_typ thy = Sign.read_typ (Theory.sign_of thy, K None);
    1.41  
    1.42  fun read_term T thy s =