diff -r 55ca0df19af5 -r 4da4fa060bb6 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Thu Jul 30 15:21:31 2009 +0200
+++ b/src/Tools/Code/code_preproc.ML	Fri Jul 31 09:34:05 2009 +0200
@@ -129,6 +129,12 @@
   #> Logic.dest_equals
   #> snd;
 
+fun same_arity thy thms =
+  let
+    val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
+    val k = fold (curry Int.max o num_args_of o Thm.prop_of) thms 0;
+  in map (Code.expand_eta thy k) thms end;
+
 fun preprocess thy c eqns =
   let
     val pre = (Simplifier.theory_context thy o #pre o the_thmproc) thy;
@@ -140,8 +146,8 @@
     |> (map o apfst) (rewrite_eqn pre)
     |> (map o apfst) (AxClass.unoverload thy)
     |> map (Code.assert_eqn thy)
-    |> burrow_fst (Code.norm_args thy)
-    |> burrow_fst (Code.norm_varnames thy)
+    |> burrow_fst (same_arity thy)
+    |> burrow_fst (Code.desymbolize_all_vars thy)
   end;
 
 fun preprocess_conv thy ct =