# HG changeset patch
# User nipkow
# Date 814611018 -3600
# Node ID 010be89a7541ffac23c9711bc73c56229b168bae
# Parent  ddfdcc9ce667d8a29ce2d133bfe368c3f0f6f2f9
Hat to modify a proof because of chaned simpset for Prod.

diff -r ddfdcc9ce667 -r 010be89a7541 src/HOL/ex/LList.ML
--- a/src/HOL/ex/LList.ML	Wed Oct 25 09:49:35 1995 +0100
+++ b/src/HOL/ex/LList.ML	Wed Oct 25 09:50:18 1995 +0100
@@ -302,10 +302,10 @@
 by (rtac allI 1);
 by (stac prem1 1);
 by (stac prem2 1);
-by (simp_tac (!simpset setloop (split_tac [expand_split,expand_sum_case])) 1);
+by (simp_tac (!simpset setloop (split_tac [expand_sum_case])) 1);
 by (strip_tac 1);
 by (res_inst_tac [("n", "n")] natE 1);
-by (res_inst_tac [("n", "xc")] natE 2);
+by (res_inst_tac [("n", "xb")] natE 2);
 by (ALLGOALS(asm_simp_tac(!simpset addsimps
             [ntrunc_0,ntrunc_one_CONS,ntrunc_CONS])));
 result();