src/HOL/Tools/datatype_package.ML
changeset 22480 b20bc8029edb
parent 22101 6d13239d5f52
child 22578 b0eb5652f210
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Mar 20 10:23:31 2007 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Mar 20 15:52:37 2007 +0100
     1.3 @@ -433,7 +433,7 @@
     1.4                   (DatatypeProp.make_tnames (map (typ_of_dtyp descr sorts) dt)),
     1.5                   case default of
     1.6                     NONE => (warning ("No clause for constructor " ^ s ^
     1.7 -                     " in case expression"); Const ("undefined", dummyT))
     1.8 +                     " in case expression"); Const ("HOL.undefined", dummyT))
     1.9                   | SOME t => t), cases)
    1.10               | SOME (c as ((_, vs), t)) =>
    1.11                   if length dt <> length vs then
    1.12 @@ -486,7 +486,7 @@
    1.13        (fold_rev count_cases cases []);
    1.14      fun mk_case1 (cname, (vs, body), _) = Syntax.const "_case1" $
    1.15        list_comb (Syntax.const cname, vs) $ body;
    1.16 -    fun is_undefined (Const ("undefined", _)) = true
    1.17 +    fun is_undefined (Const ("HOL.undefined", _)) = true
    1.18        | is_undefined _ = false;
    1.19    in
    1.20      Syntax.const "_case_syntax" $ x $