# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265797913 -3600
# Node ID 3e405c2fbe908d18ac7797c1f114d8c889cac524
# Parent  8948319b190eefa7644666cd977387e8151773cf# Parent  f24e9d21a948912be56f208aa3a9ac7dfaefcfc3
merge

diff -r 8948319b190e -r 3e405c2fbe90 Quot/Examples/LamEx.thy
--- 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
diff -r 8948319b190e -r 3e405c2fbe90 Quot/quotient_def.ML
--- 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";