1.1 --- a/src/HOL/Tools/set_comprehension_pointfree.ML	Sun Oct 14 19:16:32 2012 +0200
     1.2 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Sun Oct 14 19:16:32 2012 +0200
     1.3 @@ -264,6 +264,11 @@
     1.4  
     1.5  (* main simprocs *)
     1.6  
     1.7 +val post_thms =
     1.8 +  map mk_meta_eq [@{thm Times_Un_distrib1[symmetric]},
     1.9 +  @{lemma "A \<times> B \<union> A \<times> C = A \<times> (B \<union> C)" by auto},
    1.10 +  @{lemma "(A \<times> B \<inter> C \<times> D) = (A \<inter> C) \<times> (B \<inter> D)" by auto}]
    1.11 +
    1.12  fun conv ctxt t =
    1.13    let
    1.14      val ct = cterm_of (Proof_Context.theory_of ctxt) t
    1.15 @@ -273,8 +278,10 @@
    1.16      fun mk_thm (fm, t'') = Goal.prove ctxt [] []
    1.17        (HOLogic.mk_Trueprop (HOLogic.mk_eq (t', t''))) (fn {context, ...} => tac context fm 1)
    1.18      fun unfold th = th RS ((unfold_eq RS meta_eq_to_obj_eq) RS @{thm trans})
    1.19 +    fun post th = Conv.fconv_rule (Trueprop_conv (eq_conv Conv.all_conv
    1.20 +      (Raw_Simplifier.rewrite true post_thms))) th
    1.21    in
    1.22 -    Option.map (unfold o mk_thm) (rewrite_term t')
    1.23 +    Option.map (post o unfold o mk_thm) (rewrite_term t')
    1.24    end;
    1.25  
    1.26  fun base_simproc ss redex =