diff -r d2660637e764 -r 31c02dac5dd4 Quot/Examples/LamEx.thy
--- a/Quot/Examples/LamEx.thy	Fri Jan 15 10:36:48 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Fri Jan 15 10:48:49 2010 +0100
@@ -82,11 +82,6 @@
 as
   "rfv"
 
-thm Var_def
-thm App_def
-thm Lam_def
-thm fv_def
-
 (* definition of overloaded permutation function *)
 (* for the lifted type lam                       *)
 overloading
@@ -100,8 +95,6 @@
 
 end
 
-thm perm_lam_def
-
 (* lemmas that need to be lifted *)
 lemma pi_var_eqvt1:
   fixes pi::"'x prm"
@@ -367,17 +360,12 @@
   apply(simp add: var_supp1)
   done
 
-(* TODO: make a proper definition of substitution *)
-definition
-  subs :: "rlam \<Rightarrow> (name \<times> rlam) \<Rightarrow> rlam" ("_ \<guillemotleft>\<guillemotright> _" [70, 71] 70)
-where
-  "x \<guillemotleft>\<guillemotright> S \<equiv> x"
 
 lemma "
-  \<exists>hom\<in>Respects(alpha ===> op =). (
-    (\<forall>x. hom (rVar x) = var x) \<and>
-    (\<forall>l r. hom (rApp l r) = app (hom l) (hom r)) \<and>
-    (\<forall>x a. hom (rLam a x) = lam (\<lambda>y. hom (a \<guillemotleft>\<guillemotright> (x, rVar y)) (\<lambda>y. a \<guillemotleft>\<guillemotright> (x, rVar y))))
+  \<exists>hom \<in> Respects(alpha ===> op =). (
+    (\<forall>x. hom (rVar x) = f_var x) \<and>
+    (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and>
+    (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x)))
   )"
 
 end