# HG changeset patch
# User blanchet
# Date 1349041503 -7200
# Node ID 620fa6272c48695646700d42db897897d0314d15
# Parent  0209087a14d056b3a8e9fa3b33a4cbc67ef2e607
fixed quick-and-dirty mode

diff -r 0209087a14d0 -r 620fa6272c48 src/HOL/BNF/Tools/bnf_comp.ML
--- a/src/HOL/BNF/Tools/bnf_comp.ML	Sun Sep 30 22:02:34 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Sun Sep 30 23:45:03 2012 +0200
@@ -194,7 +194,7 @@
 
     val set_bd_tacs =
       if ! quick_and_dirty then
-        replicate (length set_alt_thms) (K all_tac)
+        replicate ilive (K all_tac)
       else
         let
           val outer_set_bds = set_bd_of_bnf outer;