# HG changeset patch
# User bulwahn
# Date 1256631885 -3600
# Node ID f47ca46d2187cf44ab510c7046065404c896dc90
# Parent  95186fb5653c9c86f25a278e8e0b5abe9ff3d7ed
disabled test case for predicate compiler due to an problem in the inductive package

diff -r 95186fb5653c -r f47ca46d2187 src/HOL/ex/Predicate_Compile_ex.thy
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Tue Oct 27 09:06:05 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Tue Oct 27 09:24:45 2009 +0100
@@ -28,7 +28,7 @@
 
 code_pred (mode: [], [1], [2], [1, 2])EmptyClosure .
 thm EmptyClosure.equation
-
+(* TODO: inductive package is broken!
 inductive False'' :: "bool"
 where
   "False \<Longrightarrow> False''"
@@ -41,7 +41,7 @@
 
 code_pred (mode: [1]) EmptySet'' .
 code_pred (mode: [], [1]) [inductify] EmptySet'' .
-
+*)
 inductive True' :: "bool"
 where
   "True \<Longrightarrow> True'"