Toplevel: generic_theory;
authorwenzelm
Wed, 11 Oct 2006 00:27:29 +0200
changeset 20956 00fe22000c6a
parent 20955 65a9a30b8ece
child 20957 f2a795db0500
Toplevel: generic_theory;
src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Oct 10 16:26:59 2006 +0200
+++ b/src/Provers/classical.ML	Wed Oct 11 00:27:29 2006 +0200
@@ -1074,7 +1074,9 @@
   OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
     OuterKeyword.diag
     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
-      (Toplevel.node_case print_claset (print_local_claset o Proof.context_of)))));
+      (Toplevel.node_case
+        (Context.cases print_claset print_local_claset)
+        (print_local_claset o Proof.context_of)))));
 
 val _ = OuterSyntax.add_parsers [print_clasetP];