diff -r 811c35e81ac5 -r 8601434fa334 src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Sun Jan 12 13:16:00 2014 +0100
+++ b/src/HOL/Tools/simpdata.ML	Sun Jan 12 14:32:22 2014 +0100
@@ -178,7 +178,7 @@
 fun hol_simplify ctxt rews =
   Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps rews);
 
-fun unfold_tac ths ctxt =
+fun unfold_tac ctxt ths =
   ALLGOALS (full_simp_tac (clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps ths));
 
 end;