changeset 34962 | 807f6ce0273d |
parent 33963 | 977b94b64905 |
child 35021 | c839a4c670c6 |
--- a/src/HOL/Tools/inductive_codegen.ML Fri Jan 22 13:39:00 2010 +0100 +++ b/src/HOL/Tools/inductive_codegen.ML Fri Jan 22 16:56:51 2010 +0100 @@ -724,7 +724,7 @@ let val (ts1, ts2) = chop k ts; val ts2' = map - (fn Bound i => Term.dummy_pattern (nth Ts i) | t => t) ts2; + (fn Bound i => Term.dummy_pattern (nth Ts (length Ts - i - 1)) | t => t) ts2; val (ots, its) = List.partition is_Bound ts2; val no_loose = forall (fn t => not (loose_bvar (t, 0))) in