src/Pure/Proof/extraction.ML
changeset 33317 b4534348b8fd
parent 33245 65232054ffd0
child 33337 9c3b9bf81e8b
     1.1 --- a/src/Pure/Proof/extraction.ML	Thu Oct 29 16:59:12 2009 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Thu Oct 29 17:58:26 2009 +0100
     1.3 @@ -651,7 +651,7 @@
     1.4                      val nt = Envir.beta_norm t;
     1.5                      val args = filter_out (fn v => member (op =) rtypes
     1.6                        (tname_of (body_type (fastype_of v)))) (vfs_of prop);
     1.7 -                    val args' = List.filter (fn v => Logic.occs (v, nt)) args;
     1.8 +                    val args' = filter (fn v => Logic.occs (v, nt)) args;
     1.9                      val t' = mkabs nt args';
    1.10                      val T = fastype_of t';
    1.11                      val cname = extr_name s vs';