tuned proofs -- avoid odd situations of polymorphic Frees in goal state;

--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Jul 27 19:27:21 2012 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Jul 27 19:57:23 2012 +0200
@@ -1051,7 +1051,7 @@
 
 lemma simplt_nb[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   shows "tmbound0 t \<Longrightarrow> bound0 (simplt t)"
-  using split0 [of "simptm t" vs bs]
+  using split0 [of "simptm t" "vs::'a list" bs]
 proof(simp add: simplt_def Let_def split_def)
   assume nb: "tmbound0 t"
   hence nb': "tmbound0 (simptm t)" by simp
@@ -1068,7 +1068,7 @@
 
 lemma simple_nb[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   shows "tmbound0 t \<Longrightarrow> bound0 (simple t)"
-  using split0 [of "simptm t" vs bs]
+  using split0 [of "simptm t" "vs::'a list" bs]
 proof(simp add: simple_def Let_def split_def)
   assume nb: "tmbound0 t"
   hence nb': "tmbound0 (simptm t)" by simp
@@ -1085,7 +1085,7 @@
 
 lemma simpeq_nb[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   shows "tmbound0 t \<Longrightarrow> bound0 (simpeq t)"
-  using split0 [of "simptm t" vs bs]
+  using split0 [of "simptm t" "vs::'a list" bs]
 proof(simp add: simpeq_def Let_def split_def)
   assume nb: "tmbound0 t"
   hence nb': "tmbound0 (simptm t)" by simp
@@ -1102,7 +1102,7 @@
 
 lemma simpneq_nb[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   shows "tmbound0 t \<Longrightarrow> bound0 (simpneq t)"
-  using split0 [of "simptm t" vs bs]
+  using split0 [of "simptm t" "vs::'a list" bs]
 proof(simp add: simpneq_def Let_def split_def)
   assume nb: "tmbound0 t"
   hence nb': "tmbound0 (simptm t)" by simp

--- a/src/HOL/GCD.thy	Fri Jul 27 19:27:21 2012 +0200
+++ b/src/HOL/GCD.thy	Fri Jul 27 19:57:23 2012 +0200
@@ -610,8 +610,8 @@
   apply (erule subst)
   apply (rule iffI)
   apply force
-  apply (drule_tac x = "abs e" in exI)
-  apply (case_tac "e >= 0")
+  apply (drule_tac x = "abs ?e" in exI)
+  apply (case_tac "(?e::int) >= 0")
   apply force
   apply force
 done

--- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Fri Jul 27 19:27:21 2012 +0200
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Fri Jul 27 19:57:23 2012 +0200
@@ -369,9 +369,6 @@
 prefer 2 apply assumption
 apply (simp add: comp_method [of G D])
 apply (erule exE)+
-apply (subgoal_tac "z =(fst z, fst (snd z), snd (snd z))")
-apply (rule exI)
-apply (simp)
 apply (simp add: split_paired_all)
 apply (intro strip)
 apply (simp add: comp_method)