diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/IOA/ABP/Lemmas.ML
--- a/src/HOL/IOA/ABP/Lemmas.ML	Wed Oct 04 13:11:57 1995 +0100
+++ b/src/HOL/IOA/ABP/Lemmas.ML	Wed Oct 04 13:12:14 1995 +0100
@@ -42,6 +42,8 @@
 
 (* Lists *)
 
+val list_ss = simpset_of "List";
+
 goal List.thy "hd(l@m) = (if l~=[] then hd(l) else hd(m))";
 by (List.list.induct_tac "l" 1);
 by (simp_tac list_ss 1);