# HG changeset patch
# User wenzelm
# Date 1354018949 -3600
# Node ID 8b0fdeeefef7232b8818cca90bf56e08c70344cf
# Parent  019d642d422d2bc796bb373d2c72e44235948516
eliminated some improper identifiers;

diff -r 019d642d422d -r 8b0fdeeefef7 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Tue Nov 27 10:56:31 2012 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Tue Nov 27 13:22:29 2012 +0100
@@ -5010,7 +5010,7 @@
   from alluopairs_set1[where xs="?U"] have UpU: "set ?Up \<le> (set ?U \<times> set ?U)" by simp
   from \<Upsilon>_l[OF lq] have U_l: "\<forall> (t,n) \<in> set ?U. numbound0 t \<and> n > 0" .
   from U_l UpU 
-  have Up_: "\<forall> ((t,n),(s,m)) \<in> set ?Up. numbound0 t \<and> n> 0 \<and> numbound0 s \<and> m > 0" by auto
+  have "\<forall> ((t,n),(s,m)) \<in> set ?Up. numbound0 t \<and> n> 0 \<and> numbound0 s \<and> m > 0" by auto
   hence Snb: "\<forall> (t,n) \<in> set ?S. numbound0 t \<and> n > 0 "
     by (auto simp add: mult_pos_pos)
   have Y_l: "\<forall> (t,n) \<in> set ?Y. numbound0 t \<and> n > 0" 
diff -r 019d642d422d -r 8b0fdeeefef7 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Nov 27 10:56:31 2012 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Nov 27 13:22:29 2012 +0100
@@ -996,9 +996,9 @@
   thus ?thesis apply- apply(rule that[of q]) unfolding True by auto next
   case False note p = division_ofD[OF assms(1)]
   have *:"\<forall>k\<in>p. \<exists>q. q division_of {a..b} \<and> k\<in>q" proof case goal1
-    guess c using p(4)[OF goal1] .. then guess d .. note cd_ = this
-    have *:"{c..d} \<subseteq> {a..b}" "{c..d} \<noteq> {}" using p(2,3)[OF goal1, unfolded cd_] using assms(2) by auto
-    guess q apply(rule partial_division_extend_1[OF *]) . thus ?case unfolding cd_ by auto qed
+    guess c using p(4)[OF goal1] .. then guess d .. note "cd" = this
+    have *:"{c..d} \<subseteq> {a..b}" "{c..d} \<noteq> {}" using p(2,3)[OF goal1, unfolded "cd"] using assms(2) by auto
+    guess q apply(rule partial_division_extend_1[OF *]) . thus ?case unfolding "cd" by auto qed
   guess q using bchoice[OF *] .. note q = conjunctD2[OF this[rule_format]]
   have "\<And>x. x\<in>p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})" apply(rule,rule_tac p="q x" in division_of_subset) proof-
     fix x assume x:"x\<in>p" show "q x division_of \<Union>q x" apply-apply(rule division_ofI)
diff -r 019d642d422d -r 8b0fdeeefef7 src/HOL/Proofs/Lambda/StrongNorm.thy
--- a/src/HOL/Proofs/Lambda/StrongNorm.thy	Tue Nov 27 10:56:31 2012 +0100
+++ b/src/HOL/Proofs/Lambda/StrongNorm.thy	Tue Nov 27 13:22:29 2012 +0100
@@ -102,7 +102,7 @@
     assume uIT: "IT u"
     assume uT: "e \<turnstile> u : T"
     {
-      case (Var rs n e_ T'_ u_ i_)
+      case (Var rs n e1 T'1 u1 i1)
       assume nT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree>\<degree> rs : T'"
       let ?ty = "\<lambda>t. \<exists>T'. e\<langle>i:T\<rangle> \<turnstile> t : T'"
       let ?R = "\<lambda>t. \<forall>e T' u i.
@@ -210,13 +210,13 @@
         with False show ?thesis by (auto simp add: subst_Var)
       qed
     next
-      case (Lambda r e_ T'_ u_ i_)
+      case (Lambda r e1 T'1 u1 i1)
       assume "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
         and "\<And>e T' u i. PROP ?Q r e T' u i T"
       with uIT uT show "IT (Abs r[u/i])"
         by fastforce
     next
-      case (Beta r a as e_ T'_ u_ i_)
+      case (Beta r a as e1 T'1 u1 i1)
       assume T: "e\<langle>i:T\<rangle> \<turnstile> Abs r \<degree> a \<degree>\<degree> as : T'"
       assume SI1: "\<And>e T' u i. PROP ?Q (r[a/0] \<degree>\<degree> as) e T' u i T"
       assume SI2: "\<And>e T' u i. PROP ?Q a e T' u i T"
diff -r 019d642d422d -r 8b0fdeeefef7 src/HOL/Proofs/Lambda/WeakNorm.thy
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Tue Nov 27 10:56:31 2012 +0100
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Tue Nov 27 13:22:29 2012 +0100
@@ -76,7 +76,7 @@
   proof induct
     fix e T' u i assume uNF: "NF u" and uT: "e \<turnstile> u : T"
     {
-      case (App ts x e_ T'_ u_ i_)
+      case (App ts x e1 T'1 u1 i1)
       assume "e\<langle>i:T\<rangle> \<turnstile> Var x \<degree>\<degree> ts : T'"
       then obtain Us
         where varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : Us \<Rrightarrow> T'"
@@ -187,7 +187,7 @@
         qed
       qed
     next
-      case (Abs r e_ T'_ u_ i_)
+      case (Abs r e1 T'1 u1 i1)
       assume absT: "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
       then obtain R S where "e\<langle>0:R\<rangle>\<langle>Suc i:T\<rangle>  \<turnstile> r : S" by (rule abs_typeE) simp
       moreover have "NF (lift u 0)" using `NF u` by (rule lift_NF)