src/HOL/Tools/datatype_package.ML

             (case find_first (equal s o fst o fst) cases' of
                NONE => (list_abs (map (rpair dummyT)
                  (DatatypeProp.make_tnames (map (typ_of_dtyp descr sorts) dt)),
                  case default of
                    NONE => (warning ("No clause for constructor " ^ s ^
-                     " in case expression"); Const ("undefined", dummyT))
+                     " in case expression"); Const ("HOL.undefined", dummyT))
                  | SOME t => t), cases)
              | SOME (c as ((_, vs), t)) =>
                  if length dt <> length vs then
                     case_error ("Wrong number of arguments for constructor " ^ s)
                       (SOME tname) vs

             (body, []) (cons cname)
     val cases' = sort (int_ord o swap o pairself (length o snd))
       (fold_rev count_cases cases []);
     fun mk_case1 (cname, (vs, body), _) = Syntax.const "_case1" $
       list_comb (Syntax.const cname, vs) $ body;
-    fun is_undefined (Const ("undefined", _)) = true
+    fun is_undefined (Const ("HOL.undefined", _)) = true
       | is_undefined _ = false;
   in
     Syntax.const "_case_syntax" $ x $
       foldr1 (fn (t, u) => Syntax.const "_case2" $ t $ u) (map mk_case1
         (case find_first (is_undefined o fst) cases' of