# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1265796644 -3600
# Node ID 67dff6c1a1238e77dc2a7524a4a5797028116a92
# Parent  c7069b09730bb386988e868b11a14681251f88de
merged

diff -r c7069b09730b -r 67dff6c1a123 Quot/Examples/LamEx.thy
--- 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
diff -r c7069b09730b -r 67dff6c1a123 Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Wed Feb 10 10:55:14 2010 +0100
+++ b/Quot/quotient_def.ML	Wed Feb 10 11:10:44 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";