# HG changeset patch
# User berghofe
# Date 1264867261 -3600
# Node ID b5c6e59e2cd721943c96f8ac90481f15236982a9
# Parent  cca208c8d619b936f773c1b38c4ea902d06a5aef
Adapted to changes in setup of cases method.

diff -r cca208c8d619 -r b5c6e59e2cd7 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Sat Jan 30 16:59:49 2010 +0100
+++ b/src/FOL/FOL.thy	Sat Jan 30 17:01:01 2010 +0100
@@ -383,6 +383,7 @@
     val atomize = @{thms induct_atomize}
     val rulify = @{thms induct_rulify}
     val rulify_fallback = @{thms induct_rulify_fallback}
+    val equal_def = @{thm induct_equal_def}
     fun dest_def _ = NONE
     fun trivial_tac _ = no_tac
   );