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 30450 7655e6533209
parent 30349 110826d1e5ff
child 31723 f5cafe803b55 
--- a/src/HOL/Tools/refute.ML	Wed Mar 11 15:56:50 2009 +0100
+++ b/src/HOL/Tools/refute.ML	Wed Mar 11 15:56:51 2009 +0100
@@ -2111,7 +2111,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 Set.empty}, HOLogic_setT)
+          val HOLogic_empty_set = HOLogic.mk_set HOLogic_prodT []
           val HOLogic_insert    =
             Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
         in
@@ -3187,7 +3187,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 Set.empty}, HOLogic_setT)
+        val HOLogic_empty_set = HOLogic.mk_set HOLogic_prodT []
         val HOLogic_insert    =
           Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
       in
isabelle