--- a/Nominal/Ex/TypeSchemes.thy	Tue Jun 14 11:43:06 2011 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Tue Jun 14 14:07:07 2011 +0100
@@ -72,11 +72,9 @@
 using assms
 by blast
 
-definition "MYUNDEFINED \<equiv> undefined"
-
 --"The following is accepted by 'function' but not by 'nominal_primrec'"
 
-function (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
+nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
     subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
 where

--- a/Nominal/Nominal2_Base.thy	Tue Jun 14 11:43:06 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Tue Jun 14 14:07:07 2011 +0100
@@ -1701,9 +1701,11 @@
   shows "Q (THE_default d P)"
 by (iprover intro: assms THE_defaultI')
 
+thm THE_default1_equality
+
 lemma the_default_eqvt:
   assumes unique: "\<exists>!x. P x"
-  shows "(p \<bullet> (THE_default d P)) = (THE_default d (p \<bullet> P))"
+  shows "(p \<bullet> (THE_default d P)) = (THE_default (p \<bullet> d) (p \<bullet> P))"
   apply(rule THE_default1_equality [symmetric])
   apply(rule_tac p="-p" in permute_boolE)
   apply(simp add: ex1_eqvt)
@@ -1716,21 +1718,37 @@
 
 lemma fundef_ex1_eqvt:
   fixes x::"'a::pt"
-  assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
+  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (G x))"
   assumes eqvt: "eqvt G"
   assumes ex1: "\<exists>!y. G x y"
   shows "(p \<bullet> (f x)) = f (p \<bullet> x)"
   apply(simp only: f_def)
   apply(subst the_default_eqvt)
   apply(rule ex1)
+  apply(rule THE_default1_equality [symmetric])
+  apply(rule_tac p="-p" in permute_boolE)
+  apply(perm_simp add: permute_minus_cancel)
   using eqvt
   unfolding eqvt_def
-  apply(simp add: permute_fun_app_eq)
+  apply(simp)
+  apply(rule ex1)
+  apply(rule_tac p="-p" in permute_boolE)
+  apply(subst permute_fun_app_eq)
+  back
+  apply(subst the_default_eqvt)
+  apply(rule_tac p="-p" in permute_boolE)
+  apply(perm_simp add: permute_minus_cancel)
+  apply(rule ex1)
+  apply(perm_simp add: permute_minus_cancel)
+  using eqvt
+  unfolding eqvt_def
+  apply(simp)
+  apply(rule THE_defaultI'[OF ex1])
   done
 
 lemma fundef_ex1_eqvt_at:
   fixes x::"'a::pt"
-  assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
+  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (G x))"
   assumes eqvt: "eqvt G"
   assumes ex1: "\<exists>!y. G x y"
   shows "eqvt_at f x"
@@ -1741,7 +1759,7 @@
 (* fixme: polish *)
 lemma fundef_ex1_prop:
   fixes x::"'a::pt"
-  assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
+  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (G x))"
   assumes P_all: "\<And>x y. G x y \<Longrightarrow> P x y"
   assumes ex1: "\<exists>!y. G x y"
   shows "P x (f x)"

--- a/Nominal/nominal_function_core.ML	Tue Jun 14 11:43:06 2011 +0100
+++ b/Nominal/nominal_function_core.ML	Tue Jun 14 14:07:07 2011 +0100
@@ -290,6 +290,7 @@
     val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,case_hyp=case_hypj,...} = ctxj
 
     val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
+
   in if j < i then
     let
       val compat = lookup_compat_thm j i cts