src/HOL/Tools/datatype_abs_proofs.ML

--- a/src/HOL/Tools/datatype_abs_proofs.ML	Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Oct 07 16:07:50 2008 +0200
@@ -291,7 +291,7 @@
       let
         val Ts = map (typ_of_dtyp descr' sorts) cargs;
         val Ts' = map mk_dummyT (List.filter is_rec_type cargs)
-      in Const ("arbitrary", Ts @ Ts' ---> T')
+      in Const (@{const_name undefined}, Ts @ Ts' ---> T')
       end) constrs) descr';
 
     val case_names = map (fn s => Sign.full_name thy1 (s ^ "_case")) new_type_names;