Removed erroneous application of rev in get_clauses that caused
authorberghofe
Fri Apr 13 15:43:25 2007 +0200 (2007-04-13)
changeset 22661f3ba63a2663e
parent 22660 2d1179ad431c
child 22662 3e492ba59355
Removed erroneous application of rev in get_clauses that caused
introduction rules taken from the InductivePackage database to
be in the wrong order.
src/HOL/Tools/inductive_codegen.ML
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Fri Apr 13 12:30:47 2007 +0200
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Fri Apr 13 15:43:25 2007 +0200
     1.3 @@ -98,7 +98,7 @@
     1.4          NONE => NONE
     1.5        | SOME ({names, ...}, {intrs, raw_induct, ...}) =>
     1.6            SOME (names, thyname_of_const s thy, length (params_of raw_induct),
     1.7 -            preprocess thy (rev intrs)))
     1.8 +            preprocess thy intrs))
     1.9      | SOME _ =>
    1.10          let
    1.11            val SOME names = find_first