src/HOL/List.ML
changeset 6141 a6922171b396
parent 6073 fba734ba6894
child 6162 484adda70b65
--- a/src/HOL/List.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/HOL/List.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -32,7 +32,7 @@
 by (REPEAT (ares_tac basic_monos 1));
 qed "lists_mono";
 
-val listsE = lists.mk_cases list.simps  "x#l : lists A";
+val listsE = lists.mk_cases "x#l : lists A";
 AddSEs [listsE];
 AddSIs lists.intrs;