--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Feb 02 01:20:28 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Feb 02 01:55:17 2012 +0100
@@ -128,14 +128,14 @@
Item_Net.content safeEs @ Item_Net.content hazEs
|> map Classical.classical_rule
val simps = ctxt |> simpset_of |> dest_ss |> #simps
- val eqs =
+ val spec_eqs =
ctxt |> Spec_Rules.get
|> filter (curry (op =) Spec_Rules.Equational o fst)
|> maps (snd o snd)
in
Termtab.empty |> add Simp I snd simps
|> add Simp atomize snd simps
- |> add Eq I I eqs
+ |> add Spec_Eq I I spec_eqs
|> add Elim I I elims
|> add Intro I I intros
end