Adapted to changes in setup of induct method.
authorberghofe
Sun, 10 Jan 2010 18:41:07 +0100
changeset 34914 e391c3de0f6b
parent 34913 d8cb720c9c53
child 34915 7894c7dab132
Adapted to changes in setup of induct method.
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
   );
 *}