diff -r a3f911785efa -r f4942eb3bb03 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Thu May 15 16:38:29 2014 +0200
+++ b/src/Tools/Code/code_preproc.ML	Thu May 15 16:38:30 2014 +0200
@@ -156,7 +156,9 @@
     val normalization =
       map2 (fn (v, sort) => fn (v', _) => (((v', 0), sort), TFree (v, sort))) vs_original vs_normalized;
   in
-    (Thm.certify_instantiate (normalization, []) o Thm.varifyT_global, cert (map_types normalize t))
+    if eq_list (eq_fst (op =)) (vs_normalized, vs_original)
+    then (I, ct)
+    else (Thm.certify_instantiate (normalization, []) o Thm.varifyT_global, cert (map_types normalize t))
   end;
 
 fun no_variables_sandwich ctxt ct =
@@ -169,7 +171,11 @@
     fun apply_beta var thm = Thm.combination thm (Thm.reflexive var)
       |> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false)))
       |> Conv.fconv_rule (Conv.arg1_conv (Thm.beta_conversion false));
-  in (fold apply_beta all_vars, fold_rev Thm.lambda all_vars ct) end;
+  in
+    if null all_vars
+    then (I, ct)
+    else (fold apply_beta all_vars, fold_rev Thm.lambda all_vars ct)
+  end;
 
 fun simplifier_conv_sandwich ctxt =
   let