--- a/CookBook/Package/simple_inductive_package.ML Sat Feb 21 11:38:14 2009 +0000
+++ b/CookBook/Package/simple_inductive_package.ML Sun Feb 22 03:44:03 2009 +0000
@@ -191,13 +191,13 @@
(* @end *)
(* @chunk syntax *)
-val ind_decl =
+val specification =
spec_parser >>
(fn (((loc, preds), params), specs) =>
Toplevel.local_theory loc (add_inductive preds params specs))
val _ = OuterSyntax.command "simple_inductive" "define inductive predicates"
- OuterKeyword.thy_decl ind_decl
+ OuterKeyword.thy_decl specification
(* @end *)
end;