--- a/Quot/Examples/LamEx.thy	Wed Feb 10 11:31:43 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Wed Feb 10 11:31:53 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

--- a/Quot/quotient_def.ML	Wed Feb 10 11:31:43 2010 +0100
+++ b/Quot/quotient_def.ML	Wed Feb 10 11:31:53 2010 +0100
@@ -73,9 +73,10 @@
 let
   val lhs = Syntax.read_term lthy lhs_str
   val rhs = Syntax.read_term lthy rhs_str
-  (* FIXME: Relating the reads will cause errors. *) 
+  val lthy' = Variable.declare_term lhs lthy
+  val lthy'' = Variable.declare_term rhs lthy'
 in
-  quotient_def mx attr lhs rhs lthy |> snd
+  quotient_def mx attr lhs rhs lthy'' |> snd
 end
 
 val _ = OuterKeyword.keyword "as";