# HG changeset patch
# User bulwahn
# Date 1257491518 -3600
# Node ID dcfe9100e0a63e7c1b00b48d453e4e8bafa650d7
# Parent  428ddcc16e7b8fe5dedc8560b0403cf664eaa2f2
disabled upt example because of a problem due to overloaded constants with the predicate compiler

diff -r 428ddcc16e7b -r dcfe9100e0a6 src/HOL/ex/Predicate_Compile_ex.thy
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Fri Nov 06 08:11:58 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Fri Nov 06 08:11:58 2009 +0100
@@ -276,6 +276,7 @@
 value [code] "Predicate.the (append_1_2 [0::int, 1, 2] [3, 4, 5])"
 value [code] "Predicate.the (append_3 ([]::int list))"
 
+
 text {* tricky case with alternative rules *}
 
 inductive append2
@@ -660,6 +661,7 @@
 thm set_of.equation
 
 code_pred [inductify] is_ord .
+thm is_ord_aux.equation
 thm is_ord.equation
 
 
@@ -714,7 +716,7 @@
 code_pred [inductify] take .
 code_pred [inductify] drop .
 code_pred [inductify] zip .
-code_pred [inductify] upt .
+(*code_pred [inductify] upt .*)
 code_pred [inductify] remdups .
 code_pred [inductify] remove1 .
 code_pred [inductify] removeAll .