--- a/Quot/Examples/LamEx.thy	Wed Feb 10 10:55:14 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Wed Feb 10 11:10:44 2010 +0100
@@ -72,8 +72,6 @@
        \<Longrightarrow> rLam a t \<approx> rLam b s"
 
 
-
-
 (* should be automatic with new version of eqvt-machinery *)
 lemma alpha_eqvt:
   fixes pi::"name prm"
@@ -253,12 +251,18 @@
     \<Longrightarrow> P lam"
   by (lifting rlam.induct)
 
+ML {* show_all_types := true *}
+
 lemma perm_lam [simp]:
   fixes pi::"'a prm"
   shows "pi \<bullet> Var a = Var (pi \<bullet> a)"
   and   "pi \<bullet> App t1 t2 = App (pi \<bullet> t1) (pi \<bullet> t2)"
   and   "pi \<bullet> Lam a t = Lam (pi \<bullet> a) (pi \<bullet> t)"
 apply(lifting perm_rlam.simps)
+ML_prf {*
+  List.last (map (symmetric o #def) (Quotient_Info.qconsts_dest @{context}));
+  List.last (map (Thm.varifyT o symmetric o #def) (Quotient_Info.qconsts_dest @{context}))
+*}
 done
 
 instance lam::pt_name