src/FOL/FOL.thy

--- a/src/FOL/FOL.thy	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/FOL/FOL.thy	Sun Nov 09 17:04:14 2014 +0100
@@ -420,7 +420,7 @@
     val rulify_fallback = @{thms induct_rulify_fallback}
     val equal_def = @{thm induct_equal_def}
     fun dest_def _ = NONE
-    fun trivial_tac _ = no_tac
+    fun trivial_tac _ _ = no_tac
   );
 *}