# HG changeset patch
# User wenzelm
# Date 1244717420 -7200
# Node ID 318081898306009dc57eb8387ad22d8ec0dec8cd
# Parent  a6c6bf2751a096e17fb3869c326b5a937a118cae
theory Predicate_Compile_ex: enable quick_and_dirty for now, to make it work with internal cheat_tac invocations;

diff -r a6c6bf2751a0 -r 318081898306 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Thu Jun 11 12:48:38 2009 +0200
+++ b/src/HOL/ex/ROOT.ML	Thu Jun 11 12:50:20 2009 +0200
@@ -14,10 +14,11 @@
   "Codegenerator_Pretty_Test",
   "NormalForm",
   "../NumberTheory/Factorization",
-  "Predicate_Compile",
-  "Predicate_Compile_ex"
+  "Predicate_Compile"
 ];
 
+setmp quick_and_dirty true use_thy "Predicate_Compile_ex";
+
 use_thys [
   "Numeral",
   "Higher_Order_Logic",