src/HOLCF/Tools/Domain/domain_axioms.ML

         let
           val dnam : string = Long_Name.base_name dname;
           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
           add_one (dnam, [("lub_take", ax)], [])
         end