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