# HG changeset patch
# User paulson
# Date 898866974 -7200
# Node ID f95e0a6eb77535d20b0a5c64ad71dffb8e860f6e
# Parent  e4aa78d1312fdf346f39150c2a4604841b2e273b
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc

diff -r e4aa78d1312f -r f95e0a6eb775 src/HOL/Induct/LList.ML
--- a/src/HOL/Induct/LList.ML	Fri Jun 26 15:10:40 1998 +0200
+++ b/src/HOL/Induct/LList.ML	Fri Jun 26 15:16:14 1998 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/ex/LList
+(*  Title:      HOL/Induct/LList
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
@@ -10,8 +10,7 @@
 
 (** Simplification **)
 
-simpset_ref() := simpset() addsplits [split_split, split_sum_case] delsimprocs [unit_eq_proc];
-
+Addsplits [split_split, split_sum_case];
 
 (*This justifies using llist in other recursive type definitions*)
 Goalw llist.defs "!!A B. A<=B ==> llist(A) <= llist(B)";