src/Provers/simplifier.ML
changeset 9513 8531c18d9181
parent 9446 7bc054e9fb1c
child 9715 5705a04d24ea
--- a/src/Provers/simplifier.ML	Thu Aug 03 18:43:35 2000 +0200
+++ b/src/Provers/simplifier.ML	Thu Aug 03 18:44:24 2000 +0200
@@ -548,7 +548,7 @@
 val print_simpsetP =
   OuterSyntax.improper_command "print_simpset" "print context of Simplifier"
     OuterSyntax.Keyword.diag
-    (Scan.succeed (Toplevel.no_timing o (Toplevel.keep
+    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
       (Toplevel.node_case print_simpset (print_local_simpset o Proof.context_of)))));
 
 val _ = OuterSyntax.add_parsers [print_simpsetP];