Adapted to changes in setup of induct method.
authorberghofe
Sun Jan 10 18:41:07 2010 +0100 (2010-01-10)
changeset 34914e391c3de0f6b
parent 34913 d8cb720c9c53
child 34915 7894c7dab132
Adapted to changes in setup of induct method.
src/FOL/FOL.thy
     1.1 --- a/src/FOL/FOL.thy	Sun Jan 10 18:39:50 2010 +0100
     1.2 +++ b/src/FOL/FOL.thy	Sun Jan 10 18:41:07 2010 +0100
     1.3 @@ -383,6 +383,8 @@
     1.4      val atomize = @{thms induct_atomize}
     1.5      val rulify = @{thms induct_rulify}
     1.6      val rulify_fallback = @{thms induct_rulify_fallback}
     1.7 +    fun dest_def _ = NONE
     1.8 +    fun trivial_tac _ = no_tac
     1.9    );
    1.10  *}
    1.11