--- a/src/HOL/Tools/inductive.ML Fri Mar 16 14:46:13 2012 +0100
+++ b/src/HOL/Tools/inductive.ML Fri Mar 16 18:20:12 2012 +0100
@@ -1144,21 +1144,21 @@
val ind_decl = gen_ind_decl add_ind_def;
val _ =
- Outer_Syntax.local_theory' "inductive" "define inductive predicates" Keyword.thy_decl
+ Outer_Syntax.local_theory' @{command_spec "inductive"} "define inductive predicates"
(ind_decl false);
val _ =
- Outer_Syntax.local_theory' "coinductive" "define coinductive predicates" Keyword.thy_decl
+ Outer_Syntax.local_theory' @{command_spec "coinductive"} "define coinductive predicates"
(ind_decl true);
val _ =
- Outer_Syntax.local_theory "inductive_cases"
- "create simplified instances of elimination rules (improper)" Keyword.thy_script
+ Outer_Syntax.local_theory @{command_spec "inductive_cases"}
+ "create simplified instances of elimination rules (improper)"
(Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
val _ =
- Outer_Syntax.local_theory "inductive_simps"
- "create simplification rules for inductive predicates" Keyword.thy_script
+ Outer_Syntax.local_theory @{command_spec "inductive_simps"}
+ "create simplification rules for inductive predicates"
(Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_simps));
end;