--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Fri Aug 27 10:56:46 2010 +0200
@@ -68,8 +68,8 @@
(*Universal quant: insert a free variable into body and continue*)
let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
in dec_sko (subst_bound (Free(fname,T), p)) rhss end
- | dec_sko (@{const "op &"} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
- | dec_sko (@{const "op |"} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
+ | dec_sko (@{const HOL.conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
+ | dec_sko (@{const HOL.disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
| dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss
| dec_sko _ rhss = rhss
in dec_sko (prop_of th) [] end;