--- a/Nominal/Ex/Lambda.thy	Wed Jun 01 11:01:39 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Wed Jun 01 13:35:37 2011 +0900
@@ -541,19 +541,6 @@
 nominal_primrec
   map_term :: "(lam \<Rightarrow> lam) \<Rightarrow> lam \<Rightarrow> lam"
 where
-  "map_term f (Var x) = f (Var x)"
-| "map_term f (App t1 t2) = App (f t1) (f t2)"
-| "map_term f (Lam [x].t) = Lam [x].(f t)"
-unfolding eqvt_def map_term_graph_def
-apply (rule, perm_simp, rule)
-apply (case_tac x, case_tac b rule: lam.exhaust)
-apply auto
-(*apply (erule Abs1_eq_fdest)*)
-oops
-
-nominal_primrec
-  map_term :: "(lam \<Rightarrow> lam) \<Rightarrow> lam \<Rightarrow> lam"
-where
   "eqvt f \<Longrightarrow> map_term f (Var x) = f (Var x)"
 | "eqvt f \<Longrightarrow> map_term f (App t1 t2) = App (f t1) (f t2)"
 | "eqvt f \<Longrightarrow> map_term f (Lam [x].t) = Lam [x].(f t)"
@@ -615,6 +602,17 @@
 | "CPS (App M N) k = CPS M (\<lambda>m. CPS N (\<lambda>n. n))"
 oops
 
+(* Problem: nominal_primrec generates non-quantified free variable "x" *)
+consts b :: name
+nominal_primrec
+  Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"
+where
+  "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))"
+unfolding eqvt_def Z_graph_def
+apply (rule, perm_simp, rule)
+prefer 2
+ML_prf {* prop_of (hd (#prems (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))))) *}
+oops
 
 (* function tests *)