src/HOL/Tools/inductive.ML
changeset 51658 21c10672633b
parent 51584 98029ceda8ce
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/Tools/inductive.ML	Tue Apr 09 13:55:28 2013 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Tue Apr 09 15:29:25 2013 +0200
     1.3 @@ -1175,8 +1175,7 @@
     1.4  val _ =
     1.5    Outer_Syntax.improper_command @{command_spec "print_inductives"}
     1.6      "print (co)inductive definitions and monotonicity rules"
     1.7 -    (Scan.succeed
     1.8 -      (Toplevel.no_timing o Toplevel.unknown_context o
     1.9 -        Toplevel.keep (print_inductives o Toplevel.context_of)));
    1.10 +    (Scan.succeed (Toplevel.unknown_context o
    1.11 +      Toplevel.keep (print_inductives o Toplevel.context_of)));
    1.12  
    1.13  end;