src/FOL/FOL.thy

--- a/src/FOL/FOL.thy	Sun Jan 10 18:39:50 2010 +0100
+++ b/src/FOL/FOL.thy	Sun Jan 10 18:41:07 2010 +0100
@@ -383,6 +383,8 @@
     val atomize = @{thms induct_atomize}
     val rulify = @{thms induct_rulify}
     val rulify_fallback = @{thms induct_rulify_fallback}
+    fun dest_def _ = NONE
+    fun trivial_tac _ = no_tac
   );
 *}