--- a/src/HOL/Tools/primrec_package.ML Tue Mar 20 10:23:31 2007 +0100
+++ b/src/HOL/Tools/primrec_package.ML Tue Mar 20 15:52:37 2007 +0100
@@ -142,7 +142,7 @@
(case AList.lookup (op =) eqns cname of
NONE => (warning ("No equation for constructor " ^ quote cname ^
"\nin definition of function " ^ quote fname);
- (fnameTs', fnss', (Const ("arbitrary", dummyT))::fns))
+ (fnameTs', fnss', (Const ("HOL.undefined", dummyT))::fns))
| SOME (ls, cargs', rs, rhs, eq) =>
let
val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
@@ -182,7 +182,7 @@
case AList.lookup (op =) fns i of
NONE =>
let
- val dummy_fns = map (fn (_, cargs) => Const ("arbitrary",
+ val dummy_fns = map (fn (_, cargs) => Const ("HOL.undefined",
replicate ((length cargs) + (length (List.filter is_rec_type cargs)))
dummyT ---> HOLogic.unitT)) constrs;
val _ = warning ("No function definition for datatype " ^ quote tname)