# HG changeset patch
# User nipkow
# Date 901523904 -7200
# Node ID a23c23af335f7d2b505b8ee005634bb37a23ec5a
# Parent  be986f7a6def4ef56d36ef108fd4139e6ae4894d
conversion bug in simpproc list_eq

diff -r be986f7a6def -r a23c23af335f src/HOL/List.ML
--- a/src/HOL/List.ML	Fri Jul 24 17:55:57 1998 +0200
+++ b/src/HOL/List.ML	Mon Jul 27 09:18:24 1998 +0200
@@ -794,7 +794,7 @@
 
 fun last (cons as Const("List.list.op #",_) $ _ $ xs) =
       (case xs of Const("List.list.[]",_) => cons | _ => last xs)
-  | last (Const("List.list.op @",_) $ _ $ ys) = last ys
+  | last (Const("List.op @",_) $ _ $ ys) = last ys
   | last t = t;
 
 fun list1 (Const("List.list.op #",_) $ _ $ Const("List.list.[]",_)) = true
@@ -802,7 +802,7 @@
 
 fun butlast ((cons as Const("List.list.op #",_) $ x) $ xs) =
       (case xs of Const("List.list.[]",_) => xs | _ => cons $ butlast xs)
-  | butlast ((app as Const("List.list.op @",_) $ xs) $ ys) = app $ butlast ys
+  | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
   | butlast xs = Const("List.list.[]",fastype_of xs);
 
 val rearr_tac =
@@ -815,7 +815,7 @@
       let val lhs1 = butlast lhs and rhs1 = butlast rhs
           val Type(_,listT::_) = eqT
           val appT = [listT,listT] ---> listT
-          val app = Const("List.list.op @",appT)
+          val app = Const("List.op @",appT)
           val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
           val ct = cterm_of sg (HOLogic.mk_Trueprop(HOLogic.mk_eq(F,F2)))
           val thm = prove_goalw_cterm [] ct (K [rearr_tac 1])