src/Tools/induct.ML

--- a/src/Tools/induct.ML	Thu Apr 16 15:11:04 2015 +0200
+++ b/src/Tools/induct.ML	Thu Apr 16 15:22:44 2015 +0200
@@ -257,8 +257,7 @@
 val _ =
   Outer_Syntax.command @{command_keyword print_induct_rules}
     "print induction and cases rules"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (print_rules o Toplevel.context_of)));
+    (Scan.succeed (Toplevel.keep (print_rules o Toplevel.context_of)));
 
 
 (* access rules *)