src/FOL/FOL.thy
changeset 58957 c9e744ea8a38
parent 58889 5b7a9633cfa8
child 59755 f8d164ab0dc1
     1.1 --- a/src/FOL/FOL.thy	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/FOL/FOL.thy	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -420,7 +420,7 @@
     1.4      val rulify_fallback = @{thms induct_rulify_fallback}
     1.5      val equal_def = @{thm induct_equal_def}
     1.6      fun dest_def _ = NONE
     1.7 -    fun trivial_tac _ = no_tac
     1.8 +    fun trivial_tac _ _ = no_tac
     1.9    );
    1.10  *}
    1.11