--- a/LList.ML Tue Feb 15 07:55:22 1994 +0100
+++ b/LList.ML Tue Feb 15 10:05:17 1994 +0100
@@ -16,7 +16,6 @@
val llist_simps = [sum_case_Inl, sum_case_Inr];
val llist_ss = univ_ss delsimps [Pair_eq]
- addsimps llist_simps
addcongs [split_weak_cong, sum_case_weak_cong]
setloop (split_tac [expand_split, expand_sum_case]);
@@ -155,8 +154,8 @@
by (stac LList_corec 1);
(*nested "sum_case"; requires an explicit split*)
by (res_inst_tac [("s", "f(xa)")] sumE 1);
-by (asm_simp_tac (univ_ss addsimps (llist_simps@[List_Fun_NIL_I])) 1);
-by (asm_simp_tac (univ_ss addsimps (llist_simps@[List_Fun_CONS_I, range_eqI])
+by (asm_simp_tac (univ_ss addsimps [List_Fun_NIL_I]) 1);
+by (asm_simp_tac (univ_ss addsimps [List_Fun_CONS_I, range_eqI]
setloop (split_tac [expand_split])) 1);
(* FIXME: can the selection of the case split be automated?
by (ASM_SIMP_TAC (llist_ss addsimps [List_Fun_CONS_I, rangeI]) 1);*)