Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/inductive_package.ML
changeset 28524 644b62cf678f
parent 28107 760ecc6fc1bd
child 28791 cc16be808796 
--- a/src/HOL/Tools/inductive_package.ML	Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Tue Oct 07 16:07:50 2008 +0200
@@ -212,7 +212,7 @@
       else apsnd (cons p) (find_arg T x ps);
 
 fun make_args Ts xs =
-  map (fn (T, (NONE, ())) => Const ("arbitrary", T) | (_, (SOME t, ())) => t)
+  map (fn (T, (NONE, ())) => Const (@{const_name undefined}, T) | (_, (SOME t, ())) => t)
     (fold (fn (t, T) => snd o find_arg T t) xs (map (rpair (NONE, ())) Ts));
 
 fun make_args' Ts xs Us =
isabelle