# HG changeset patch
# User blanchet
# Date 1328655922 -3600
# Node ID 93344b60cb301b2d429e6fb934404d74cde5304d
# Parent  9552b6f2c6704a2759f2f50f20e4bddf88f3bdb3
beware of "Bit0" and "Bit1" -- these shouldn't be blidly unfolded by SPASS, lest we get gigantic terms

diff -r 9552b6f2c670 -r 93344b60cb30 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Feb 06 23:01:02 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Feb 08 00:05:22 2012 +0100
@@ -115,6 +115,9 @@
   map_aterms (fn Var ((s, _), T) => Var ((s, 0), T) | t => t)
   #> map_types (map_type_tvar (fn ((s, _), S) => TVar ((s, 0), S)))
 
+(* unfolding these can yield really huge terms *)
+val risky_spec_eqs = @{thms Bit0_def Bit1_def}
+
 fun clasimpset_rule_table_of ctxt =
   let
     val thy = Proof_Context.theory_of ctxt
@@ -132,6 +135,7 @@
       ctxt |> Spec_Rules.get
            |> filter (curry (op =) Spec_Rules.Equational o fst)
            |> maps (snd o snd)
+           |> filter_out (member Thm.eq_thm_prop risky_spec_eqs)
   in
     Termtab.empty |> add Simp I snd simps
                   |> add Simp atomize snd simps