# HG changeset patch
# User wenzelm
# Date 968876977 -7200
# Node ID 5610c4acb48d3b661cfc1f8565d4f98c3c7dfc69
# Parent  879e88b1e5522970e8c83a7ccdb7c820fb4952a7
LFilter: setmp quick_and_dirty false;

diff -r 879e88b1e552 -r 5610c4acb48d src/HOL/Induct/ROOT.ML
--- a/src/HOL/Induct/ROOT.ML	Wed Sep 13 22:29:17 2000 +0200
+++ b/src/HOL/Induct/ROOT.ML	Wed Sep 13 22:29:37 2000 +0200
@@ -10,6 +10,7 @@
 time_use_thy "MultisetOrder";
 time_use_thy "PropLog";
 time_use_thy "SList";
+setmp quick_and_dirty false     (* FIXME tmp hack *)
 time_use_thy "LFilter";
 time_use_thy "Term";
 time_use_thy "ABexp";