# HG changeset patch
# User bulwahn
# Date 1349858841 -7200
# Node ID bed063d0c5266d51e4d2b9028804811ada10998c
# Parent  b5e355c41de3736067ded8b029bf14c85e425367
generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)

diff -r b5e355c41de3 -r bed063d0c526 src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Oct 10 10:41:18 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Oct 10 10:47:21 2012 +0200
@@ -150,15 +150,23 @@
     |> Option.map (fn thm => thm RS @{thm eq_reflection})
   end;
 
-(* FIXME: turn into generic simproc for many predicates, i.e., remove hard-coded finite! *)
+fun instantiate_arg_cong ctxt pred =
+  let
+    val certify = cterm_of (Proof_Context.theory_of ctxt)
+    val arg_cong = @{thm arg_cong}
+    val f $ _ = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (concl_of arg_cong)))
+  in
+    cterm_instantiate [(certify f, certify pred)] arg_cong
+  end;
+
 fun simproc ss redex =
   let
     val ctxt = Simplifier.the_context ss
-    val _ $ set_compr = term_of redex
+    val pred $ set_compr = term_of redex
+    val arg_cong' = instantiate_arg_cong ctxt pred
   in
     conv ctxt set_compr
-    |> Option.map (fn thm =>
-         thm RS @{thm arg_cong[of _ _ finite]} RS @{thm eq_reflection})
+    |> Option.map (fn thm => thm RS arg_cong' RS @{thm eq_reflection})
   end;
 
 fun code_simproc ss redex =