src/HOL/Tools/inductive_package.ML
changeset 6723 f342449d73ca
parent 6556 daa00919502b
child 6729 b6e167580a32
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Mon May 24 21:56:14 1999 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon May 24 21:57:13 1999 +0200
     1.3 @@ -704,20 +704,23 @@
     1.4  
     1.5  (* outer syntax *)
     1.6  
     1.7 -local open OuterParse in
     1.8 +local structure P = OuterParse and K = OuterSyntax.Keyword in
     1.9  
    1.10  fun mk_ind coind (((sets, (atts, intrs)), monos), con_defs) =
    1.11 -  #1 o add_inductive true coind sets atts (map triple_swap intrs) monos con_defs;
    1.12 +  #1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs;
    1.13  
    1.14  fun ind_decl coind =
    1.15 -  Scan.repeat1 term --
    1.16 -  ($$$ "intrs" |-- !!! (opt_attribs -- Scan.repeat1 (opt_thm_name ":" -- term))) --
    1.17 -  Scan.optional ($$$ "monos" |-- !!! xthms1) [] --
    1.18 -  Scan.optional ($$$ "con_defs" |-- !!! xthms1) []
    1.19 +  Scan.repeat1 P.term --
    1.20 +  (P.$$$ "intrs" |-- P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.term))) --
    1.21 +  Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) [] --
    1.22 +  Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1) []
    1.23    >> (Toplevel.theory o mk_ind coind);
    1.24  
    1.25 -val inductiveP = OuterSyntax.command "inductive" "define inductive sets" (ind_decl false);
    1.26 -val coinductiveP = OuterSyntax.command "coinductive" "define coinductive sets" (ind_decl true);
    1.27 +val inductiveP =
    1.28 +  OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false);
    1.29 +
    1.30 +val coinductiveP =
    1.31 +  OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true);
    1.32  
    1.33  val _ = OuterSyntax.add_keywords ["intrs", "monos", "con_defs"];
    1.34  val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP];