src/HOL/Tools/inductive.ML
changeset 36960 01594f816e3a
parent 36958 ad5313f1bd30
child 37264 8b931fb51cc6
     1.1 --- a/src/HOL/Tools/inductive.ML	Mon May 17 15:11:25 2010 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Mon May 17 23:54:15 2010 +0200
     1.3 @@ -970,32 +970,28 @@
     1.4  
     1.5  (* outer syntax *)
     1.6  
     1.7 -local structure P = OuterParse and K = OuterKeyword in
     1.8 -
     1.9 -val _ = OuterKeyword.keyword "monos";
    1.10 +val _ = Keyword.keyword "monos";
    1.11  
    1.12  fun gen_ind_decl mk_def coind =
    1.13 -  P.fixes -- P.for_fixes --
    1.14 +  Parse.fixes -- Parse.for_fixes --
    1.15    Scan.optional Parse_Spec.where_alt_specs [] --
    1.16 -  Scan.optional (P.$$$ "monos" |-- P.!!! Parse_Spec.xthms1) []
    1.17 +  Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) []
    1.18    >> (fn (((preds, params), specs), monos) =>
    1.19        (snd oo gen_add_inductive mk_def true coind preds params specs monos));
    1.20  
    1.21  val ind_decl = gen_ind_decl add_ind_def;
    1.22  
    1.23  val _ =
    1.24 -  OuterSyntax.local_theory' "inductive" "define inductive predicates" K.thy_decl
    1.25 +  Outer_Syntax.local_theory' "inductive" "define inductive predicates" Keyword.thy_decl
    1.26      (ind_decl false);
    1.27  
    1.28  val _ =
    1.29 -  OuterSyntax.local_theory' "coinductive" "define coinductive predicates" K.thy_decl
    1.30 +  Outer_Syntax.local_theory' "coinductive" "define coinductive predicates" Keyword.thy_decl
    1.31      (ind_decl true);
    1.32  
    1.33  val _ =
    1.34 -  OuterSyntax.local_theory "inductive_cases"
    1.35 -    "create simplified instances of elimination rules (improper)" K.thy_script
    1.36 -    (P.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
    1.37 +  Outer_Syntax.local_theory "inductive_cases"
    1.38 +    "create simplified instances of elimination rules (improper)" Keyword.thy_script
    1.39 +    (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
    1.40  
    1.41  end;
    1.42 -
    1.43 -end;