diff -r d069f23e941f -r 55d8e38262a8 src/HOL/List.ML
--- a/src/HOL/List.ML	Fri Aug 16 11:27:10 1996 +0200
+++ b/src/HOL/List.ML	Mon Aug 19 11:12:38 1996 +0200
@@ -80,19 +80,19 @@
 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed "mem_filter";
 
-(** setOfList **)
+(** set_of_list **)
 
-goal thy "setOfList (xs@ys) = (setOfList xs Un setOfList ys)";
+goal thy "set_of_list (xs@ys) = (set_of_list xs Un set_of_list ys)";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 by (Fast_tac 1);
-qed "setOfList_append";
+qed "set_of_list_append";
 
-goal thy "(x mem xs) = (x: setOfList xs)";
+goal thy "(x mem xs) = (x: set_of_list xs)";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 by (Fast_tac 1);
-qed "setOfList_mem_eq";
+qed "set_of_list_mem_eq";
 
 
 (** list_all **)