src/Pure/Isar/isar_cmd.ML
changeset 35141 182f27a8716c
parent 33671 4b0f2599ed48
child 35852 4e3fe0b8687b
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Feb 16 11:56:13 2010 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Feb 16 11:59:05 2010 +0100
     1.3 @@ -332,16 +332,14 @@
     1.4  val print_abbrevs = Toplevel.unknown_context o
     1.5    Toplevel.keep (ProofContext.print_abbrevs o Toplevel.context_of);
     1.6  
     1.7 -val print_facts = Toplevel.unknown_context o Toplevel.keep (fn state =>
     1.8 -  ProofContext.setmp_verbose_CRITICAL
     1.9 -    ProofContext.print_lthms (Toplevel.context_of state));
    1.10 +val print_facts = Toplevel.unknown_context o
    1.11 +  Toplevel.keep (ProofContext.print_lthms o Toplevel.context_of);
    1.12  
    1.13 -val print_configs = Toplevel.unknown_context o Toplevel.keep (fn state =>
    1.14 -  Attrib.print_configs (Toplevel.context_of state));
    1.15 +val print_configs = Toplevel.unknown_context o
    1.16 +  Toplevel.keep (Attrib.print_configs o Toplevel.context_of);
    1.17  
    1.18 -val print_theorems_proof = Toplevel.keep (fn state =>
    1.19 -  ProofContext.setmp_verbose_CRITICAL
    1.20 -    ProofContext.print_lthms (Proof.context_of (Toplevel.proof_of state)));
    1.21 +val print_theorems_proof =
    1.22 +  Toplevel.keep (ProofContext.print_lthms o Proof.context_of o Toplevel.proof_of);
    1.23  
    1.24  fun print_theorems_theory verbose = Toplevel.keep (fn state =>
    1.25    Toplevel.theory_of state |>
    1.26 @@ -430,11 +428,11 @@
    1.27  
    1.28  (* print proof context contents *)
    1.29  
    1.30 -val print_binds = Toplevel.unknown_context o Toplevel.keep (fn state =>
    1.31 -  ProofContext.setmp_verbose_CRITICAL ProofContext.print_binds (Toplevel.context_of state));
    1.32 +val print_binds = Toplevel.unknown_context o
    1.33 +  Toplevel.keep (ProofContext.print_binds o Toplevel.context_of);
    1.34  
    1.35 -val print_cases = Toplevel.unknown_context o Toplevel.keep (fn state =>
    1.36 -  ProofContext.setmp_verbose_CRITICAL ProofContext.print_cases (Toplevel.context_of state));
    1.37 +val print_cases = Toplevel.unknown_context o
    1.38 +  Toplevel.keep (ProofContext.print_cases o Toplevel.context_of);
    1.39  
    1.40  
    1.41  (* print theorems, terms, types etc. *)