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/HOL/Tools/SMT/smt_monomorph.ML
changeset 38864 4abe644fcea5
parent 36898 8e55aa1306c5
child 39020 ac0f24f850c9 
--- a/src/HOL/Tools/SMT/smt_monomorph.ML	Sat Aug 28 20:24:40 2010 +0800
+++ b/src/HOL/Tools/SMT/smt_monomorph.ML	Sat Aug 28 16:14:32 2010 +0200
@@ -16,7 +16,7 @@
 
 val ignored = member (op =) [
   @{const_name All}, @{const_name Ex}, @{const_name Let}, @{const_name If},
-  @{const_name "op ="}, @{const_name zero_class.zero},
+  @{const_name HOL.eq}, @{const_name zero_class.zero},
   @{const_name one_class.one}, @{const_name number_of}]
 
 fun is_const f (n, T) = not (ignored n) andalso f T
isabelle