# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265625685 -3600
# Node ID 30550327651aa5a4ee018267de89b1cb30138a00
# Parent  f8029d8c88a970b16bece2962cccd0af923c60eb
Proper context fixes lifting inside instantiations.

diff -r f8029d8c88a9 -r 30550327651a Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Mon Feb 08 10:47:19 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Mon Feb 08 11:41:25 2010 +0100
@@ -403,9 +403,11 @@
 as
   "permute :: perm \<Rightarrow> trm \<Rightarrow> trm"
 
+lemmas permute_ktt[simp] = permute_kind_permute_ty_permute_trm.simps[quot_lifted]
+
 lemma perm_zero_ok: "0 \<bullet> (x :: KIND) = x \<and> 0 \<bullet> (y :: TY) = y \<and> 0 \<bullet> (z :: TRM) = z"
 apply (induct rule: KIND_TY_TRM_induct)
-apply (simp_all add: permute_kind_permute_ty_permute_trm.simps[quot_lifted])
+apply (simp_all)
 done
 
 lemma perm_add_ok:
@@ -413,7 +415,7 @@
   "((p + q) \<bullet> (x2 :: TY) = p \<bullet> q \<bullet> x2)"
   "((p + q) \<bullet> (x3 :: TRM) = p \<bullet> q \<bullet> x3)"
 apply (induct x1 and x2 and x3 rule: KIND_TY_TRM_inducts)
-apply (simp_all add: permute_kind_permute_ty_permute_trm.simps[quot_lifted])
+apply (simp_all)
 done
 
 instance
@@ -423,8 +425,6 @@
 
 end
 
-lemmas permute_ktt[simp] = permute_kind_permute_ty_permute_trm.simps[quot_lifted]
-
 lemmas AKIND_ATY_ATRM_inducts = akind_aty_atrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
 lemmas KIND_TY_TRM_INJECT = akind_aty_atrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
diff -r f8029d8c88a9 -r 30550327651a Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Mon Feb 08 10:47:19 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Mon Feb 08 11:41:25 2010 +0100
@@ -214,16 +214,16 @@
 as
   "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"
 
+lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted]
+
 instance
 apply default
 apply(induct_tac [!] x rule: trm1_bp_inducts(1))
-apply(simp_all add: permute_rtrm1_permute_bp.simps[quot_lifted])
+apply(simp_all)
 done
 
 end
 
-lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted]
-
 lemmas fv_trm1 = rfv_trm1_rfv_bp.simps[quot_lifted]
 
 lemmas fv_trm1_eqvt = rfv_trm1_eqvt[quot_lifted]
diff -r f8029d8c88a9 -r 30550327651a Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Mon Feb 08 10:47:19 2010 +0100
+++ b/Quot/quotient_tacs.ML	Mon Feb 08 11:41:25 2010 +0100
@@ -653,8 +653,8 @@
 let
   val ctxt = Context.proof_of context
   val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt
-  val goal = (quotient_lift_all ctxt o prop_of) thm'
-  val nthm = Goal.prove ctxt [] [] goal (fn x => lift_tac ctxt [thm] 1)
+  val goal = (quotient_lift_all ctxt' o prop_of) thm'
+  val nthm = Goal.prove ctxt' [] [] goal (fn x => lift_tac ctxt' [thm] 1)
   val [nthm1] = ProofContext.export ctxt' ctxt [nthm]
 in
   nthm1