src/HOL/Tools/refute.ML

           val pairss = map (map HOLogic.mk_prod) functions
           (* Term.typ *)
           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
           (* functions as graphs, i.e. as a (HOL) set of pairs "(x, y)" *)
           map (List.foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc)

           (constants ~~ results)
         (* Term.typ *)
         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
         SOME (List.foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc)
           HOLogic_empty_set pairs)