diff -r fa103abdbade -r 2c04e30c2f3e src/HOL/BNF/Tools/bnf_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_tactics.ML	Wed Sep 18 15:33:31 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML	Wed Sep 18 15:33:32 2013 +0200
@@ -51,7 +51,8 @@
     rtac (Drule.instantiate_normalize insts thm) 1
   end);
 
-fun unfold_thms_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms);
+fun unfold_thms_tac _ [] = all_tac
+  | unfold_thms_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms);
 
 fun mk_unfold_thms_then_tac lthy defs tac x = unfold_thms_tac lthy defs THEN tac x;