diff -r 52771c21d9ca -r 14b9286ed036 llist.ML
--- a/llist.ML	Wed Apr 06 16:31:06 1994 +0200
+++ b/llist.ML	Tue Apr 19 10:50:00 1994 +0200
@@ -483,10 +483,9 @@
 
 (** Two easy results about Lmap **)
 
-val [prem] = goal LList.thy
+val [prem] = goalw LList.thy [o_def]
     "M: LList(A) ==> Lmap(f o g, M) = Lmap(f, Lmap(g, M))";
 by (rtac (prem RS imageI RS LList_equalityI) 1);
-by (stac o_def 1);
 by (safe_tac set_cs);
 by (etac LListE 1);
 by (ALLGOALS (asm_simp_tac (HOL_ss addsimps [Lmap_NIL,Lmap_CONS])));