changeset 27332 | 94790a9620c3 |
parent 26571 | 114da911bc41 |
child 29606 | fedb8be05f24 |
--- a/src/Pure/conv.ML Mon Jun 23 23:45:44 2008 +0200 +++ b/src/Pure/conv.ML Mon Jun 23 23:45:45 2008 +0200 @@ -133,7 +133,7 @@ (*rewrite B in !!x1 ... xn. B*) fun params_conv n cv ctxt ct = - if n <> 0 andalso can Logic.dest_all (Thm.term_of ct) + if n <> 0 andalso Logic.is_all (Thm.term_of ct) then arg_conv (abs_conv (params_conv (n - 1) cv o #2) ctxt) ct else cv ctxt ct;