src/Provers/classical.ML
changeset 42439 9efdd0af15ac
parent 42361 23f352990944
child 42790 e07e56300faa
     1.1 --- a/src/Provers/classical.ML	Wed Apr 20 17:17:01 2011 +0200
     1.2 +++ b/src/Provers/classical.ML	Wed Apr 20 22:57:29 2011 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4  sig
     1.5    type claset
     1.6    val empty_cs: claset
     1.7 -  val print_cs: claset -> unit
     1.8 +  val print_cs: Proof.context -> claset -> unit
     1.9    val rep_cs:
    1.10      claset -> {safeIs: thm list, safeEs: thm list,
    1.11                   hazIs: thm list, hazEs: thm list,
    1.12 @@ -258,8 +258,8 @@
    1.13       dup_netpair   = empty_netpair,
    1.14       xtra_netpair  = empty_netpair};
    1.15  
    1.16 -fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) =
    1.17 -  let val pretty_thms = map Display.pretty_thm_without_context in
    1.18 +fun print_cs ctxt (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) =
    1.19 +  let val pretty_thms = map (Display.pretty_thm ctxt) in
    1.20      [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
    1.21        Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
    1.22        Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
    1.23 @@ -1018,6 +1018,8 @@
    1.24    Outer_Syntax.improper_command "print_claset" "print context of Classical Reasoner"
    1.25      Keyword.diag
    1.26      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    1.27 -      Toplevel.keep (print_cs o claset_of o Toplevel.context_of)));
    1.28 +      Toplevel.keep (fn state =>
    1.29 +        let val ctxt = Toplevel.context_of state
    1.30 +        in print_cs ctxt (claset_of ctxt) end)));
    1.31  
    1.32  end;