src/Pure/primitive_defs.ML

--- a/src/Pure/primitive_defs.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/Pure/primitive_defs.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -74,7 +74,7 @@
     val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq));
     val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (vars, body));
     val (lhs', args) = Term.strip_comb lhs;
-    val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs);
+    val rhs' = fold_rev (absfree o dest_Free) args rhs;
   in (lhs', rhs') end;
 
 end;