src/HOL/UNITY/UNITY_Main.thy

--- a/src/HOL/UNITY/UNITY_Main.thy	Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/UNITY/UNITY_Main.thy	Fri May 13 23:58:40 2011 +0200
@@ -19,4 +19,10 @@
   (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
 *} "for proving progress properties"
 
+setup {*
+  Simplifier.map_simpset_global (fn ss => ss
+    addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair})
+    addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map}))
+*}
+
 end