src/HOL/List.ML
changeset 5200 a23c23af335f
parent 5183 89f162de39cf
child 5272 95cfd872fe66
     1.1 --- a/src/HOL/List.ML	Fri Jul 24 17:55:57 1998 +0200
     1.2 +++ b/src/HOL/List.ML	Mon Jul 27 09:18:24 1998 +0200
     1.3 @@ -794,7 +794,7 @@
     1.4  
     1.5  fun last (cons as Const("List.list.op #",_) $ _ $ xs) =
     1.6        (case xs of Const("List.list.[]",_) => cons | _ => last xs)
     1.7 -  | last (Const("List.list.op @",_) $ _ $ ys) = last ys
     1.8 +  | last (Const("List.op @",_) $ _ $ ys) = last ys
     1.9    | last t = t;
    1.10  
    1.11  fun list1 (Const("List.list.op #",_) $ _ $ Const("List.list.[]",_)) = true
    1.12 @@ -802,7 +802,7 @@
    1.13  
    1.14  fun butlast ((cons as Const("List.list.op #",_) $ x) $ xs) =
    1.15        (case xs of Const("List.list.[]",_) => xs | _ => cons $ butlast xs)
    1.16 -  | butlast ((app as Const("List.list.op @",_) $ xs) $ ys) = app $ butlast ys
    1.17 +  | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
    1.18    | butlast xs = Const("List.list.[]",fastype_of xs);
    1.19  
    1.20  val rearr_tac =
    1.21 @@ -815,7 +815,7 @@
    1.22        let val lhs1 = butlast lhs and rhs1 = butlast rhs
    1.23            val Type(_,listT::_) = eqT
    1.24            val appT = [listT,listT] ---> listT
    1.25 -          val app = Const("List.list.op @",appT)
    1.26 +          val app = Const("List.op @",appT)
    1.27            val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
    1.28            val ct = cterm_of sg (HOLogic.mk_Trueprop(HOLogic.mk_eq(F,F2)))
    1.29            val thm = prove_goalw_cterm [] ct (K [rearr_tac 1])