Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/term.ML
changeset 20664 ffbc5a57191a
parent 20548 8ef25fe585a8
child 20854 f9cf9e62d11c 
--- a/src/Pure/term.ML	Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Pure/term.ML	Thu Sep 21 19:04:20 2006 +0200
@@ -964,7 +964,7 @@
 fun is_first_order quants =
   let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body
         | first_order1 Ts (Const(q,_) $ Abs(a,T,body)) =
-            q mem_string quants  andalso   (*it is a known quantifier*)
+            member (op =) quants q  andalso   (*it is a known quantifier*)
             not (is_funtype T)   andalso first_order1 (T::Ts) body
         | first_order1 Ts t =
             case strip_comb t of
isabelle