--- a/src/Provers/classical.ML Tue Apr 09 13:55:28 2013 +0200
+++ b/src/Provers/classical.ML Tue Apr 09 15:29:25 2013 +0200
@@ -968,9 +968,6 @@
val _ =
Outer_Syntax.improper_command @{command_spec "print_claset"} "print context of Classical Reasoner"
- (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
- Toplevel.keep (fn state =>
- let val ctxt = Toplevel.context_of state
- in print_claset ctxt end)));
+ (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_claset o Toplevel.context_of)));
end;