1.1 --- a/src/ZF/Tools/inductive_package.ML	Mon May 17 15:11:25 2010 +0200
     1.2 +++ b/src/ZF/Tools/inductive_package.ML	Mon May 17 23:54:15 2010 +0200
     1.3 @@ -576,29 +576,26 @@
     1.4  
     1.5  (* outer syntax *)
     1.6  
     1.7 -local structure P = OuterParse and K = OuterKeyword in
     1.8 -
     1.9 -val _ = List.app OuterKeyword.keyword
    1.10 +val _ = List.app Keyword.keyword
    1.11    ["domains", "intros", "monos", "con_defs", "type_intros", "type_elims"];
    1.12  
    1.13  fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) =
    1.14 -  #1 o add_inductive doms (map P.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);
    1.15 +  #1 o add_inductive doms (map Parse.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);
    1.16  
    1.17  val ind_decl =
    1.18 -  (P.$$$ "domains" |-- P.!!! (P.enum1 "+" P.term --
    1.19 -      ((P.$$$ "\<subseteq>" || P.$$$ "<=") |-- P.term))) --
    1.20 -  (P.$$$ "intros" |--
    1.21 -    P.!!! (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- P.prop))) --
    1.22 -  Scan.optional (P.$$$ "monos" |-- P.!!! Parse_Spec.xthms1) [] --
    1.23 -  Scan.optional (P.$$$ "con_defs" |-- P.!!! Parse_Spec.xthms1) [] --
    1.24 -  Scan.optional (P.$$$ "type_intros" |-- P.!!! Parse_Spec.xthms1) [] --
    1.25 -  Scan.optional (P.$$$ "type_elims" |-- P.!!! Parse_Spec.xthms1) []
    1.26 +  (Parse.$$$ "domains" |-- Parse.!!! (Parse.enum1 "+" Parse.term --
    1.27 +      ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<=") |-- Parse.term))) --
    1.28 +  (Parse.$$$ "intros" |--
    1.29 +    Parse.!!! (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop))) --
    1.30 +  Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) [] --
    1.31 +  Scan.optional (Parse.$$$ "con_defs" |-- Parse.!!! Parse_Spec.xthms1) [] --
    1.32 +  Scan.optional (Parse.$$$ "type_intros" |-- Parse.!!! Parse_Spec.xthms1) [] --
    1.33 +  Scan.optional (Parse.$$$ "type_elims" |-- Parse.!!! Parse_Spec.xthms1) []
    1.34    >> (Toplevel.theory o mk_ind);
    1.35  
    1.36 -val _ = OuterSyntax.command (co_prefix ^ "inductive")
    1.37 -  ("define " ^ co_prefix ^ "inductive sets") K.thy_decl ind_decl;
    1.38 +val _ =
    1.39 +  Outer_Syntax.command (co_prefix ^ "inductive")
    1.40 +    ("define " ^ co_prefix ^ "inductive sets") Keyword.thy_decl ind_decl;
    1.41  
    1.42  end;
    1.43  
    1.44 -end;
    1.45 -