src/HOL/Tools/inductive.ML

--- a/src/HOL/Tools/inductive.ML	Thu Apr 16 15:11:04 2015 +0200
+++ b/src/HOL/Tools/inductive.ML	Thu Apr 16 15:22:44 2015 +0200
@@ -1190,7 +1190,6 @@
 val _ =
   Outer_Syntax.command @{command_keyword print_inductives}
     "print (co)inductive definitions and monotonicity rules"
-    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
-      Toplevel.keep (print_inductives b o Toplevel.context_of)));
+    (Parse.opt_bang >> (fn b => Toplevel.keep (print_inductives b o Toplevel.context_of)));
 
 end;