src/HOL/Tools/inductive.ML
changeset 46961 5c6955f487e5
parent 46949 94aa7b81bcf6
child 47876 0521ee2e504d
     1.1 --- a/src/HOL/Tools/inductive.ML	Fri Mar 16 14:46:13 2012 +0100
     1.2 +++ b/src/HOL/Tools/inductive.ML	Fri Mar 16 18:20:12 2012 +0100
     1.3 @@ -1144,21 +1144,21 @@
     1.4  val ind_decl = gen_ind_decl add_ind_def;
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.local_theory' "inductive" "define inductive predicates" Keyword.thy_decl
     1.8 +  Outer_Syntax.local_theory' @{command_spec "inductive"} "define inductive predicates"
     1.9      (ind_decl false);
    1.10  
    1.11  val _ =
    1.12 -  Outer_Syntax.local_theory' "coinductive" "define coinductive predicates" Keyword.thy_decl
    1.13 +  Outer_Syntax.local_theory' @{command_spec "coinductive"} "define coinductive predicates"
    1.14      (ind_decl true);
    1.15  
    1.16  val _ =
    1.17 -  Outer_Syntax.local_theory "inductive_cases"
    1.18 -    "create simplified instances of elimination rules (improper)" Keyword.thy_script
    1.19 +  Outer_Syntax.local_theory @{command_spec "inductive_cases"}
    1.20 +    "create simplified instances of elimination rules (improper)"
    1.21      (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
    1.22  
    1.23  val _ =
    1.24 -  Outer_Syntax.local_theory "inductive_simps"
    1.25 -    "create simplification rules for inductive predicates" Keyword.thy_script
    1.26 +  Outer_Syntax.local_theory @{command_spec "inductive_simps"}
    1.27 +    "create simplification rules for inductive predicates"
    1.28      (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_simps));
    1.29  
    1.30  end;