# HG changeset patch
# User bulwahn
# Date 1295463678 -3600
# Node ID 79dae6b7857de28d3f1a82332d2feeee7a105d8d
# Parent  0f98d8f27912abea47fb884faed36f37f20d0e05
fixing list_to_set_comprehension simproc

diff -r 0f98d8f27912 -r 79dae6b7857d src/HOL/Tools/list_to_set_comprehension.ML
--- a/src/HOL/Tools/list_to_set_comprehension.ML	Wed Jan 19 21:46:45 2011 +0100
+++ b/src/HOL/Tools/list_to_set_comprehension.ML	Wed Jan 19 20:01:18 2011 +0100
@@ -47,6 +47,11 @@
     Const (@{const_name HOL.conj}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
   | _ => raise CTERM ("conj_conv", [ct]));
 
+fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th)
+  
+fun conjunct_assoc_conv ct = Conv.try_conv
+    ((rewr_conv' @{thm conj_assoc}) then_conv conj_conv Conv.all_conv conjunct_assoc_conv) ct
+  
 fun right_hand_set_comprehension_conv conv ctxt = Trueprop_conv (eq_conv Conv.all_conv
   (Collect_conv (all_exists_conv conv o #2) ctxt))
 
@@ -54,8 +59,6 @@
  
 datatype termlets = If | Case of (typ * int)
 
-fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th)
-
 fun simproc ss redex =
   let
     val ctxt = Simplifier.the_context ss
@@ -136,7 +139,7 @@
                     (eq_conv Conv.all_conv (rewr_conv' (List.last prems))
                     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 conjunct_assoc_conv)) context
                 then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
                   Conv.repeat_conv (all_but_last_exists_conv (K (rewr_conv' @{thm simp_thms(39)})) ctxt)) context)))) 1) ctxt 1
             THEN tac ctxt cont
@@ -172,7 +175,7 @@
           if eqs = [] then NONE (* no rewriting, nothing to be done *)
           else
             let
-              val Type (@{type_name List.list}, [rT]) = fastype_of t
+              val Type (@{type_name List.list}, [rT]) = fastype_of1 (map snd bound_vs, t)
               val pat_eq =
                 case try dest_singleton_list t of
                   SOME t' => Const (@{const_name HOL.eq}, rT --> rT --> @{typ bool})