diff -r b66034025548 -r 52c35a59bbf5 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -978,27 +978,27 @@
 
 lemma lt: "numnoabs t \<Longrightarrow> Ifm bs (split lt (rsplit0 t)) = Ifm bs (Lt t) \<and> isrlfm (split lt (rsplit0 t))"
 using rsplit0[where bs = "bs" and t="t"]
-by (auto simp add: lt_def split_def,cases "snd(rsplit0 t)",auto,case_tac "nat",auto)
+by (auto simp add: lt_def split_def,cases "snd(rsplit0 t)",auto,rename_tac nat a b,case_tac "nat",auto)
 
 lemma le: "numnoabs t \<Longrightarrow> Ifm bs (split le (rsplit0 t)) = Ifm bs (Le t) \<and> isrlfm (split le (rsplit0 t))"
 using rsplit0[where bs = "bs" and t="t"]
-by (auto simp add: le_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto)
+by (auto simp add: le_def split_def) (cases "snd(rsplit0 t)",auto,rename_tac nat a b,case_tac "nat",auto)
 
 lemma gt: "numnoabs t \<Longrightarrow> Ifm bs (split gt (rsplit0 t)) = Ifm bs (Gt t) \<and> isrlfm (split gt (rsplit0 t))"
 using rsplit0[where bs = "bs" and t="t"]
-by (auto simp add: gt_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto)
+by (auto simp add: gt_def split_def) (cases "snd(rsplit0 t)",auto,rename_tac nat a b,case_tac "nat",auto)
 
 lemma ge: "numnoabs t \<Longrightarrow> Ifm bs (split ge (rsplit0 t)) = Ifm bs (Ge t) \<and> isrlfm (split ge (rsplit0 t))"
 using rsplit0[where bs = "bs" and t="t"]
-by (auto simp add: ge_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto)
+by (auto simp add: ge_def split_def) (cases "snd(rsplit0 t)",auto,rename_tac nat a b,case_tac "nat",auto)
 
 lemma eq: "numnoabs t \<Longrightarrow> Ifm bs (split eq (rsplit0 t)) = Ifm bs (Eq t) \<and> isrlfm (split eq (rsplit0 t))"
 using rsplit0[where bs = "bs" and t="t"]
-by (auto simp add: eq_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto)
+by (auto simp add: eq_def split_def) (cases "snd(rsplit0 t)",auto,rename_tac nat a b,case_tac "nat",auto)
 
 lemma neq: "numnoabs t \<Longrightarrow> Ifm bs (split neq (rsplit0 t)) = Ifm bs (NEq t) \<and> isrlfm (split neq (rsplit0 t))"
 using rsplit0[where bs = "bs" and t="t"]
-by (auto simp add: neq_def split_def) (cases "snd(rsplit0 t)",auto,case_tac "nat",auto)
+by (auto simp add: neq_def split_def) (cases "snd(rsplit0 t)",auto,rename_tac nat a b,case_tac "nat",auto)
 
 lemma conj_lin: "isrlfm p \<Longrightarrow> isrlfm q \<Longrightarrow> isrlfm (conj p q)"
 by (auto simp add: conj_def)