1.1 --- a/src/HOL/Tools/set_comprehension_pointfree.ML	Mon Jun 25 16:03:21 2012 +0200
     1.2 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Mon Jun 25 18:21:18 2012 +0200
     1.3 @@ -1,14 +1,14 @@
     1.4 -(*  Title:      HOL/ex/set_comprehension_pointfree.ML
     1.5 +(*  Title:      HOL/Tools/set_comprehension_pointfree.ML
     1.6      Author:     Felix Kuperjans, Lukas Bulwahn, TU Muenchen
     1.7 -                Rafal Kolanski, NICTA
     1.8 +    Author:     Rafal Kolanski, NICTA
     1.9  
    1.10  Simproc for rewriting set comprehensions to pointfree expressions.
    1.11  *)
    1.12  
    1.13  signature SET_COMPREHENSION_POINTFREE =
    1.14  sig
    1.15 -  val code_simproc : morphism -> simpset -> cterm -> thm option
    1.16 -  val simproc : morphism -> simpset -> cterm -> thm option
    1.17 +  val code_simproc : simpset -> cterm -> thm option
    1.18 +  val simproc : simpset -> cterm -> thm option
    1.19    val rewrite_term : term -> term option
    1.20    (* FIXME: function conv is not a conversion, i.e. of type cterm -> thm, MAYBE rename *)
    1.21    val conv : Proof.context -> term -> thm option
    1.22 @@ -143,7 +143,7 @@
    1.23  
    1.24  (* simproc *)
    1.25  
    1.26 -fun base_simproc _ ss redex =
    1.27 +fun base_simproc ss redex =
    1.28    let
    1.29      val ctxt = Simplifier.the_context ss
    1.30      val set_compr = term_of redex
    1.31 @@ -153,7 +153,7 @@
    1.32    end;
    1.33  
    1.34  (* FIXME: turn into generic simproc for many predicates, i.e., remove hard-coded finite! *)
    1.35 -fun simproc _ ss redex =
    1.36 +fun simproc ss redex =
    1.37    let
    1.38      val ctxt = Simplifier.the_context ss
    1.39      val _ $ set_compr = term_of redex
    1.40 @@ -163,11 +163,11 @@
    1.41           thm RS @{thm arg_cong[of _ _ finite]} RS @{thm eq_reflection})
    1.42    end;
    1.43  
    1.44 -fun code_simproc morphism ss redex =
    1.45 +fun code_simproc ss redex =
    1.46    let
    1.47      val prep_thm = Raw_Simplifier.rewrite false @{thms eq_equal[symmetric]} redex
    1.48    in
    1.49 -    case base_simproc morphism ss (Thm.rhs_of prep_thm) of
    1.50 +    case base_simproc ss (Thm.rhs_of prep_thm) of
    1.51        SOME rewr_thm => SOME (transitive_thm OF [transitive_thm OF [prep_thm, rewr_thm],
    1.52          Raw_Simplifier.rewrite false @{thms eq_equal} (Thm.rhs_of rewr_thm)])
    1.53      | NONE => NONE