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 30307 6c74ef5a349f
parent 30275 381ce8d88cb8
parent 30305 720226bedc4d
child 30312 0e0cb7ac0281 
--- a/src/HOL/Tools/refute.ML	Fri Mar 06 09:35:43 2009 +0100
+++ b/src/HOL/Tools/refute.ML	Fri Mar 06 11:10:57 2009 +0100
@@ -2094,7 +2094,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
@@ -3159,7 +3159,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