UNIV is not a logical constant
authorhuffman
Tue, 02 Mar 2010 04:53:18 -0800
changeset 35499 6acef0aea07d
parent 35498 5c70de748522
child 35501 5d88ffdb290c
child 35512 d1ef88d7de5a
UNIV is not a logical constant
src/HOLCF/Tools/Domain/domain_axioms.ML
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Tue Mar 02 04:35:44 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Tue Mar 02 04:53:18 2010 -0800
@@ -154,7 +154,7 @@
           val take_const = %%:(dname^"_take");
           val lub = %%: @{const_name lub};
           val image = %%: @{const_name image};
-          val UNIV = %%: @{const_name UNIV};
+          val UNIV = @{term "UNIV :: nat set"};
           val lhs = lub $ (image $ take_const $ UNIV);
           val ax = mk_trp (lhs === ID);
         in