removed redundant hd_append variant;

--- a/src/HOLCF/IOA/ABP/Correctness.thy	Mon Apr 14 21:44:53 2008 +0200
+++ b/src/HOLCF/IOA/ABP/Correctness.thy	Mon Apr 14 22:29:56 2008 +0200
@@ -83,8 +83,8 @@
     "l ~= [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))"
   apply simp
   apply (tactic {* auto_tac (@{claset},
-    HOL_ss addsplits [thm"list.split"]
-    addsimps (thms "reverse.simps" @ [thm "hd_append", thm "rev_red_not_nil"])) *})
+    HOL_ss addsplits [@{thm list.split}]
+    addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}])) *})
   done
 
 text {* Main Lemma 1 for @{text "S_pkt"} in showing that reduce is refinement. *}

--- a/src/HOLCF/IOA/ABP/Lemmas.thy	Mon Apr 14 21:44:53 2008 +0200
+++ b/src/HOLCF/IOA/ABP/Lemmas.thy	Mon Apr 14 22:29:56 2008 +0200
@@ -39,9 +39,6 @@
 
 subsection {* Lists *}
 
-lemma hd_append: "hd(l@m) = (if l~=[] then hd(l) else hd(m))"
-  by (induct l) simp_all
-
 lemma cons_not_nil: "l ~= [] --> (? x xs. l = (x#xs))"
   by (induct l) simp_all