src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML

 
 val crude_zero_vars =
   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
     val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy
     fun add stature g f =

     val simps = ctxt |> simpset_of |> dest_ss |> #simps
     val spec_eqs =
       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
                   |> add Spec_Eq I I spec_eqs
                   |> add Elim I I elims