diff -r 6069098854b9 -r 477380c74c1d src/HOLCF/IOA/ABP/Lemmas.ML
--- a/src/HOLCF/IOA/ABP/Lemmas.ML	Thu Feb 19 17:57:54 2004 +0100
+++ b/src/HOLCF/IOA/ABP/Lemmas.ML	Thu Feb 19 18:24:08 2004 +0100
@@ -37,16 +37,14 @@
 
 (* Lists *)
 
-val list_ss = simpset_of List.thy;
-
-goal List.thy "hd(l@m) = (if l~=[] then hd(l) else hd(m))";
+Goal "hd(l@m) = (if l~=[] then hd(l) else hd(m))";
 by (induct_tac "l" 1);
-by (simp_tac list_ss 1);
-by (simp_tac list_ss 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
 val hd_append =result();
 
-goal List.thy "l ~= [] --> (? x xs. l = (x#xs))";
+Goal "l ~= [] --> (? x xs. l = (x#xs))";
  by (induct_tac "l" 1);
- by (simp_tac list_ss 1);
+ by (Simp_tac 1);
  by (Fast_tac 1);
 qed"cons_not_nil";