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