src/Tools/induct.ML
changeset 46961 5c6955f487e5
parent 45375 7fe19930dfc9
child 47060 e2741ec9ae36
     1.1 --- a/src/Tools/induct.ML	Fri Mar 16 14:46:13 2012 +0100
     1.2 +++ b/src/Tools/induct.ML	Fri Mar 16 18:20:12 2012 +0100
     1.3 @@ -259,8 +259,9 @@
     1.4    end;
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.improper_command "print_induct_rules" "print induction and cases rules"
     1.8 -    Keyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
     1.9 +  Outer_Syntax.improper_command @{command_spec "print_induct_rules"}
    1.10 +    "print induction and cases rules"
    1.11 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    1.12        Toplevel.keep (print_rules o Toplevel.context_of)));
    1.13  
    1.14