--- a/Nominal/Ex/Lambda.thy	Tue May 18 17:17:54 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Tue May 18 17:56:41 2010 +0200
@@ -508,6 +508,10 @@
 | "subst_raw (Lam_raw x t) y s =
      (if x = y then t else
        (if atom x \<notin> (fv_lam_raw s) then (Lam_raw x (subst_raw t y s)) else undefined))"
+(* termination/lifting fail with sth like:
+| "subst_raw (Lam_raw x t) y s =
+     (FRESH v. Lam_raw v (subst_raw (subst_var_raw t x v) y s))"
+*)
 
 quotient_definition
   subst ("_ [ _ ::= _ ]" [100,100,100] 100)