# HG changeset patch
# User wenzelm
# Date 898784000 -7200
# Node ID ef479934678be226948c9adef52feafc1db08597
# Parent  8e5a7942fdead9b00389e9afe1fcf36d39c45ec5
delsimprocs [unit_eq_proc];

diff -r 8e5a7942fdea -r ef479934678b src/HOL/Induct/LList.ML
--- a/src/HOL/Induct/LList.ML	Thu Jun 25 16:12:02 1998 +0200
+++ b/src/HOL/Induct/LList.ML	Thu Jun 25 16:13:20 1998 +0200
@@ -10,7 +10,7 @@
 
 (** Simplification **)
 
-simpset_ref() := simpset() addsplits [split_split, split_sum_case];
+simpset_ref() := simpset() addsplits [split_split, split_sum_case] delsimprocs [unit_eq_proc];
 
 
 (*This justifies using llist in other recursive type definitions*)