1.1 --- a/src/HOL/Tools/inductive_package.ML	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -923,6 +923,8 @@
     1.4  
     1.5  local structure P = OuterParse and K = OuterKeyword in
     1.6  
     1.7 +val _ = OuterSyntax.keywords ["monos"];
     1.8 +
     1.9  (* FIXME tmp *)
    1.10  fun flatten_specification specs = specs |> maps
    1.11    (fn (a, (concl, [])) => concl |> map
    1.12 @@ -945,22 +947,15 @@
    1.13  
    1.14  val ind_decl = gen_ind_decl add_ind_def;
    1.15  
    1.16 -val inductiveP =
    1.17 -  OuterSyntax.command "inductive" "define inductive predicates" K.thy_decl (ind_decl false);
    1.18 +val _ = OuterSyntax.command "inductive" "define inductive predicates" K.thy_decl (ind_decl false);
    1.19 +val _ = OuterSyntax.command "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true);
    1.20  
    1.21 -val coinductiveP =
    1.22 -  OuterSyntax.command "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true);
    1.23 -
    1.24 -
    1.25 -val inductive_casesP =
    1.26 +val _ =
    1.27    OuterSyntax.command "inductive_cases"
    1.28      "create simplified instances of elimination rules (improper)" K.thy_script
    1.29      (P.opt_target -- P.and_list1 SpecParse.spec
    1.30        >> (fn (loc, specs) => Toplevel.local_theory loc (snd o inductive_cases specs)));
    1.31  
    1.32 -val _ = OuterSyntax.add_keywords ["monos"];
    1.33 -val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
    1.34 -
    1.35  end;
    1.36  
    1.37  end;