# HG changeset patch
# User berghofe
# Date 1263145267 -3600
# Node ID e391c3de0f6bd741a74b0df88d6b5d9e04cb3637
# Parent  d8cb720c9c5395738077488841715d5fea1936e1
Adapted to changes in setup of induct method.

diff -r d8cb720c9c53 -r e391c3de0f6b 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
   );
 *}