src/HOL/Nominal/nominal_primrec.ML
changeset 28524 644b62cf678f
parent 28083 103d9282a946
child 28965 1de908189869
     1.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Tue Oct 07 16:07:40 2008 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Tue Oct 07 16:07:50 2008 +0200
     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 (@{const_name 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 @@ -183,7 +183,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 (@{const_name 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)