# HG changeset patch
# User paulson
# Date 905441316 -7200
# Node ID 0e26af5975ba91b8ce835d628951e12d0f609c3a
# Parent  367878234bb29cdbc24d8829c30c32057706e7d5
in_set_butlast_appendI supersedes in_set_butlast_appendI1,2

diff -r 367878234bb2 -r 0e26af5975ba src/HOL/Lex/RegSet_of_nat_DA.ML
--- a/src/HOL/Lex/RegSet_of_nat_DA.ML	Thu Sep 10 17:27:50 1998 +0200
+++ b/src/HOL/Lex/RegSet_of_nat_DA.ML	Thu Sep 10 17:28:36 1998 +0200
@@ -4,8 +4,8 @@
     Copyright   1998 TUM
 *)
 
-Addsimps [in_set_butlast_appendI1,in_set_butlast_appendI2];
-AddIs    [in_set_butlast_appendI1,in_set_butlast_appendI2];
+Addsimps [in_set_butlast_appendI];
+AddIs    [in_set_butlast_appendI];
 Addsimps [image_eqI];
 
 (* Lists *)