src/Tools/Code/code_preproc.ML

   #> f
   #> Thm.prop_of
   #> 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;
     val functrans = (map (fn (_, (_, f)) => f thy) o #functrans
       o the_thmproc) thy;

     eqns
     |> apply_functrans thy c functrans
     |> (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 =
   let
     val pre = (Simplifier.theory_context thy o #pre o the_thmproc) thy;