CookBook/Package/simple_inductive_package.ML
changeset 129 e0d368a45537
parent 124 0b9fa606a746
child 159 64fa844064fa
--- 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;