# HG changeset patch
# User wenzelm
# Date 1285936071 -7200
# Node ID d466bd29c887aeba84680df0caa99b528ea5bb3e
# Parent  cdee5ca9ba9e17c756805c2b1f998cc4f6e3d0f3
more antiquotations;

diff -r cdee5ca9ba9e -r d466bd29c887 src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Fri Oct 01 13:36:35 2010 +0200
+++ b/src/HOL/Tools/primrec.ML	Fri Oct 01 14:27:51 2010 +0200
@@ -146,7 +146,7 @@
       (case AList.lookup (op =) eqns cname of
         NONE => (warning ("No equation for constructor " ^ quote cname ^
           "\nin definition of function " ^ quote fname);
-            (fnames', fnss', (Const ("HOL.undefined", dummyT)) :: fns))
+            (fnames', fnss', (Const (@{const_name undefined}, dummyT)) :: fns))
       | SOME (ls, cargs', rs, rhs, eq) =>
           let
             val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
@@ -185,7 +185,7 @@
   (case AList.lookup (op =) fns i of
     NONE =>
       let
-        val dummy_fns = map (fn (_, cargs) => Const ("HOL.undefined",
+        val dummy_fns = map (fn (_, cargs) => Const (@{const_name undefined},
           replicate (length cargs + length (filter is_rec_type cargs))
             dummyT ---> HOLogic.unitT)) constrs;
         val _ = warning ("No function definition for datatype " ^ quote tname)