1.1 --- a/src/Pure/Isar/code.ML	Mon Sep 29 12:31:59 2008 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Mon Sep 29 12:32:00 2008 +0200
     1.3 @@ -134,8 +134,9 @@
     1.4      val thy = Thm.theory_of_thm thm;
     1.5      val args_of = snd o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
     1.6      val args = args_of thm;
     1.7 +    val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
     1.8      fun matches_args args' = length args <= length args' andalso
     1.9 -      Pattern.matchess thy (args, curry Library.take (length args) args');
    1.10 +      Pattern.matchess thy (args, (map incr_idx o curry Library.take (length args)) args');
    1.11      fun drop (thm', linear') = if (linear orelse not linear')
    1.12        andalso matches_args (args_of thm') then 
    1.13          (warning ("Code generator: dropping redundant defining equation\n" ^ Display.string_of_thm thm'); true)
    1.14 @@ -368,7 +369,7 @@
    1.15            (Pretty.block o Pretty.breaks) (
    1.16              Pretty.str s
    1.17              :: Pretty.str "="
    1.18 -            :: separate (Pretty.str "|") (map (fn (c, []) => Pretty.str c
    1.19 +            :: separate (Pretty.str "|") (map (fn (c, []) => Pretty.str (Code_Unit.string_of_const thy c)
    1.20                   | (c, tys) =>
    1.21                       (Pretty.block o Pretty.breaks)
    1.22                          (Pretty.str (Code_Unit.string_of_const thy c)