--- a/src/HOL/ex/SList.ML Fri Aug 16 11:27:10 1996 +0200
+++ b/src/HOL/ex/SList.ML Mon Aug 19 11:12:38 1996 +0200
@@ -277,23 +277,23 @@
(*** Unfolding the basic combinators ***)
-val [null_Nil,null_Cons] = list_recs null_def;
-val [_,hd_Cons] = list_recs hd_def;
-val [_,tl_Cons] = list_recs tl_def;
-val [ttl_Nil,ttl_Cons] = list_recs ttl_def;
-val [append_Nil3,append_Cons] = list_recs append_def;
-val [mem_Nil, mem_Cons] = list_recs mem_def;
-val [setOfList_Nil,setOfList_Cons] = list_recs setOfList_def;
-val [map_Nil,map_Cons] = list_recs map_def;
-val [list_case_Nil,list_case_Cons] = list_recs list_case_def;
-val [filter_Nil,filter_Cons] = list_recs filter_def;
+val [null_Nil, null_Cons] = list_recs null_def;
+val [_, hd_Cons] = list_recs hd_def;
+val [_, tl_Cons] = list_recs tl_def;
+val [ttl_Nil, ttl_Cons] = list_recs ttl_def;
+val [append_Nil3, append_Cons] = list_recs append_def;
+val [mem_Nil, mem_Cons] = list_recs mem_def;
+val [set_of_list_Nil, set_of_list_Cons] = list_recs set_of_list_def;
+val [map_Nil, map_Cons] = list_recs map_def;
+val [list_case_Nil, list_case_Cons] = list_recs list_case_def;
+val [filter_Nil, filter_Cons] = list_recs filter_def;
Addsimps
[null_Nil, ttl_Nil,
mem_Nil, mem_Cons,
list_case_Nil, list_case_Cons,
append_Nil3, append_Cons,
- setOfList_Nil, setOfList_Cons,
+ set_of_list_Nil, set_of_list_Cons,
map_Nil, map_Cons,
filter_Nil, filter_Cons];