# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1307536355 -32400
# Node ID 1233af5cea95c16d8bff702b105e3fb23ed59d4e
# Parent  80bbb023402577460f94b5d0bdae3e336230bfd4
Issue with 'default'

diff -r 80bbb0234025 -r 1233af5cea95 Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Wed Jun 08 12:30:56 2011 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Wed Jun 08 21:32:35 2011 +0900
@@ -71,9 +71,12 @@
 using assms
 by blast
 
+--"The following two terms have the same type, however the first one is a valid default, but the second one no"
 definition "MYUNDEFINED \<equiv> undefined"
+term "\<lambda>(x :: (name \<times> ty) list \<times> ty + (name \<times> ty) list \<times> tys). MYUNDEFINED :: ty + tys"
+term "\<lambda>(x :: (name \<times> ty) list \<times> ty + (name \<times> ty) list \<times> tys). sum_case (\<lambda>x. Inl (undefined :: ty)) (\<lambda>x. Inr (undefined :: tys)) x"
 
-nominal_primrec (default "\<lambda>x. MYUNDEFINED")
+nominal_primrec (default "\<lambda>(x :: (name \<times> ty) list \<times> ty + (name \<times> ty) list \<times> tys). MYUNDEFINED :: ty + tys")
     subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
 where