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/refute.ML
changeset 30304 d8e4cd2ac2a1
parent 29956 62f931b257b7
child 30305 720226bedc4d 
--- a/src/HOL/Tools/refute.ML	Thu Mar 05 08:23:10 2009 +0100
+++ b/src/HOL/Tools/refute.ML	Thu Mar 05 08:23:11 2009 +0100
@@ -2089,7 +2089,7 @@
           val HOLogic_prodT = HOLogic.mk_prodT (T1, T2)
           val HOLogic_setT  = HOLogic.mk_setT HOLogic_prodT
           (* Term.term *)
-          val HOLogic_empty_set = Const (@{const_name "{}"}, HOLogic_setT)
+          val HOLogic_empty_set = Const (@{const_name Set.empty}, HOLogic_setT)
           val HOLogic_insert    =
             Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
         in
@@ -3154,7 +3154,7 @@
         val HOLogic_prodT = HOLogic.mk_prodT (T1, T2)
         val HOLogic_setT  = HOLogic.mk_setT HOLogic_prodT
         (* Term.term *)
-        val HOLogic_empty_set = Const (@{const_name "{}"}, HOLogic_setT)
+        val HOLogic_empty_set = Const (@{const_name Set.empty}, HOLogic_setT)
         val HOLogic_insert    =
           Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
       in
isabelle