src/ZF/Tools/induct_tacs.ML
changeset 22101 6d13239d5f52
parent 21350 6e58289b6685
child 22846 fb79144af9a3
     1.1 --- a/src/ZF/Tools/induct_tacs.ML	Fri Jan 19 22:08:07 2007 +0100
     1.2 +++ b/src/ZF/Tools/induct_tacs.ML	Fri Jan 19 22:08:08 2007 +0100
     1.3 @@ -199,10 +199,10 @@
     1.4  local structure P = OuterParse and K = OuterKeyword in
     1.5  
     1.6  val rep_datatype_decl =
     1.7 -  (P.$$$ "elimination" |-- P.!!! P.xthm) --
     1.8 -  (P.$$$ "induction" |-- P.!!! P.xthm) --
     1.9 -  (P.$$$ "case_eqns" |-- P.!!! P.xthms1) --
    1.10 -  Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! P.xthms1) []
    1.11 +  (P.$$$ "elimination" |-- P.!!! SpecParse.xthm) --
    1.12 +  (P.$$$ "induction" |-- P.!!! SpecParse.xthm) --
    1.13 +  (P.$$$ "case_eqns" |-- P.!!! SpecParse.xthms1) --
    1.14 +  Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! SpecParse.xthms1) []
    1.15    >> (fn (((x, y), z), w) => rep_datatype x y z w);
    1.16  
    1.17  val rep_datatypeP =