# HG changeset patch
# User wenzelm
# Date 1340630047 -7200
# Node ID 87c831e30f0ab99c4dab3f1a3dfc69457a94aaea
# Parent  fa7c0c659798120eed81003c74acb6e9b530c691
ignore morphism more explicitly;
tuned headers;

diff -r fa7c0c659798 -r 87c831e30f0a CONTRIBUTORS
--- a/CONTRIBUTORS	Mon Jun 25 14:21:32 2012 +0200
+++ b/CONTRIBUTORS	Mon Jun 25 15:14:07 2012 +0200
@@ -9,6 +9,7 @@
 * June 2012: Felix Kuperjans, Lukas Bulwahn, TUM and Rafal Kolanski, NICTA
   Simproc for rewriting set comprehensions into pointfree expressions
 
+
 Contributions to Isabelle2012
 -----------------------------
 
diff -r fa7c0c659798 -r 87c831e30f0a src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Jun 25 14:21:32 2012 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Jun 25 15:14:07 2012 +0200
@@ -20,7 +20,7 @@
 use "Tools/set_comprehension_pointfree.ML"
 
 simproc_setup finite_Collect ("finite (Collect P)") =
-  {* Set_Comprehension_Pointfree.simproc *}
+  {* K Set_Comprehension_Pointfree.simproc *}
 
 
 lemma finite_induct [case_names empty insert, induct set: finite]:
diff -r fa7c0c659798 -r 87c831e30f0a src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Mon Jun 25 14:21:32 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Mon Jun 25 15:14:07 2012 +0200
@@ -1,13 +1,13 @@
-(*  Title:      HOL/ex/set_comprehension_pointfree.ML
+(*  Title:      HOL/Tools/set_comprehension_pointfree.ML
     Author:     Felix Kuperjans, Lukas Bulwahn, TU Muenchen
-                Rafal Kolanski, NICTA
+    Author:     Rafal Kolanski, NICTA
 
 Simproc for rewriting set comprehensions to pointfree expressions.
 *)
 
 signature SET_COMPREHENSION_POINTFREE =
 sig
-  val simproc : morphism -> simpset -> cterm -> thm option
+  val simproc : simpset -> cterm -> thm option
   val rewrite_term : term -> term option
   val conv : Proof.context -> term -> thm option
 end
@@ -141,7 +141,7 @@
 
 (* simproc *)
 
-fun simproc _ ss redex =
+fun simproc ss redex =
   let
     val ctxt = Simplifier.the_context ss
     val _ $ set_compr = term_of redex