1.1 --- a/src/Tools/induct.ML Sat Oct 06 16:41:22 2007 +0200
1.2 +++ b/src/Tools/induct.ML Sat Oct 06 16:50:04 2007 +0200
1.3 @@ -161,10 +161,10 @@
1.4 |> Pretty.chunks |> Pretty.writeln
1.5 end;
1.6
1.7 -val _ = OuterSyntax.add_parsers [
1.8 +val _ =
1.9 OuterSyntax.improper_command "print_induct_rules" "print induction and cases rules"
1.10 OuterKeyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
1.11 - Toplevel.keep (print_rules o Toplevel.context_of)))];
1.12 + Toplevel.keep (print_rules o Toplevel.context_of)));
1.13
1.14
1.15 (* access rules *)