src/HOL/Tools/primrec_package.ML
changeset 22480 b20bc8029edb
parent 22101 6d13239d5f52
child 22692 1e057a3f087d
     1.1 --- a/src/HOL/Tools/primrec_package.ML	Tue Mar 20 10:23:31 2007 +0100
     1.2 +++ b/src/HOL/Tools/primrec_package.ML	Tue Mar 20 15:52:37 2007 +0100
     1.3 @@ -142,7 +142,7 @@
     1.4        (case AList.lookup (op =) eqns cname of
     1.5            NONE => (warning ("No equation for constructor " ^ quote cname ^
     1.6              "\nin definition of function " ^ quote fname);
     1.7 -              (fnameTs', fnss', (Const ("arbitrary", dummyT))::fns))
     1.8 +              (fnameTs', fnss', (Const ("HOL.undefined", dummyT))::fns))
     1.9          | SOME (ls, cargs', rs, rhs, eq) =>
    1.10              let
    1.11                val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
    1.12 @@ -182,7 +182,7 @@
    1.13    case AList.lookup (op =) fns i of
    1.14       NONE =>
    1.15         let
    1.16 -         val dummy_fns = map (fn (_, cargs) => Const ("arbitrary",
    1.17 +         val dummy_fns = map (fn (_, cargs) => Const ("HOL.undefined",
    1.18             replicate ((length cargs) + (length (List.filter is_rec_type cargs)))
    1.19               dummyT ---> HOLogic.unitT)) constrs;
    1.20           val _ = warning ("No function definition for datatype " ^ quote tname)