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/function_package/lexicographic_order.ML
changeset 30304 d8e4cd2ac2a1
parent 29713 55c30d1117ef
child 30493 b8570ea1ce25 
--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Thu Mar 05 08:23:10 2009 +0100
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Thu Mar 05 08:23:11 2009 +0100
@@ -24,7 +24,7 @@
     let 
         val relT = HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))
         val mlexT = (domT --> HOLogic.natT) --> relT --> relT
-        fun mk_ms [] = Const (@{const_name "{}"}, relT)
+        fun mk_ms [] = Const (@{const_name Set.empty}, relT)
           | mk_ms (f::fs) = 
             Const (@{const_name "mlex_prod"}, mlexT) $ f $ mk_ms fs
     in
isabelle