--- a/src/HOL/Prolog/prolog.ML Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/Prolog/prolog.ML Sun Nov 27 23:10:19 2011 +0100
@@ -62,7 +62,7 @@
(Simplifier.global_context @{theory} empty_ss
|> Simplifier.set_mksimps (mksimps mksimps_pairs))
addsimps [
- all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
+ @{thm all_conj_distrib}, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
imp_conjR, (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
imp_all]; (* "((!x. D) :- G) = (!x. D :- G)" *)