# HG changeset patch
# User wenzelm
# Date 1160519249 -7200
# Node ID 00fe22000c6a01bae3a842dd65cbde867ba065f9
# Parent  65a9a30b8ece6ee6088800df10916a4f42f3dc39
Toplevel: generic_theory;

diff -r 65a9a30b8ece -r 00fe22000c6a 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];