src/ZF/Tools/ind_cases.ML
changeset 24867 e5b55d7be9bb
parent 24508 c8b82fec6447
child 27691 ce171cbd4b93
     1.1 --- a/src/ZF/Tools/ind_cases.ML	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/ZF/Tools/ind_cases.ML	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -76,15 +76,11 @@
     1.4  
     1.5  local structure P = OuterParse and K = OuterKeyword in
     1.6  
     1.7 -val ind_cases =
     1.8 -  P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop)
     1.9 -  >> (Toplevel.theory o inductive_cases);
    1.10 -
    1.11 -val inductive_casesP =
    1.12 +val _ =
    1.13    OuterSyntax.command "inductive_cases"
    1.14 -    "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
    1.15 -
    1.16 -val _ = OuterSyntax.add_parsers [inductive_casesP];
    1.17 +    "create simplified instances of elimination rules (improper)" K.thy_script
    1.18 +    (P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop)
    1.19 +      >> (Toplevel.theory o inductive_cases));
    1.20  
    1.21  end;
    1.22