# HG changeset patch
# User krauss
# Date 1294763883 -3600
# Node ID 2aec4b8cd289309ab08e7b21e32ffeb598b7f992
# Parent  f1e7e244dcf5bdeb25b5340845c5dc6f7edf1a15
eliminated duplication

diff -r f1e7e244dcf5 -r 2aec4b8cd289 src/HOL/Tools/list_to_set_comprehension.ML
--- a/src/HOL/Tools/list_to_set_comprehension.ML	Tue Jan 11 17:00:21 2011 +0100
+++ b/src/HOL/Tools/list_to_set_comprehension.ML	Tue Jan 11 17:38:03 2011 +0100
@@ -54,9 +54,7 @@
  
 datatype termlets = If | Case of (typ * int)
 
-fun meta_eq th = th RS @{thm eq_reflection}
-
-fun rewr_conv' th = Conv.rewr_conv (meta_eq th)
+fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th)
 
 fun simproc ss redex =
   let
@@ -136,7 +134,7 @@
               CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K
                   ((conj_conv 
                     (eq_conv Conv.all_conv (rewr_conv' (List.last prems))
-                    then_conv (Conv.try_conv (Conv.rewrs_conv (map meta_eq (#inject info))))) Conv.all_conv)
+                    then_conv (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq (#inject info))))) Conv.all_conv)
                     then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq))
                     then_conv (Conv.try_conv (rewr_conv' @{thm conj_assoc})))) context
                 then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>