src/HOL/List.ML
changeset 7224 e41e64476f9b
parent 7032 d6efb3b8e669
child 7246 33058867d6eb
     1.1 --- a/src/HOL/List.ML	Mon Aug 16 22:04:07 1999 +0200
     1.2 +++ b/src/HOL/List.ML	Mon Aug 16 22:07:12 1999 +0200
     1.3 @@ -253,18 +253,18 @@
     1.4  val list_eq_pattern =
     1.5    Thm.read_cterm (Theory.sign_of List.thy) ("(xs::'a list) = ys",HOLogic.boolT);
     1.6  
     1.7 -fun last (cons as Const("List.list.op #",_) $ _ $ xs) =
     1.8 -      (case xs of Const("List.list.[]",_) => cons | _ => last xs)
     1.9 +fun last (cons as Const("List.list.Cons",_) $ _ $ xs) =
    1.10 +      (case xs of Const("List.list.Nil",_) => cons | _ => last xs)
    1.11    | last (Const("List.op @",_) $ _ $ ys) = last ys
    1.12    | last t = t;
    1.13  
    1.14 -fun list1 (Const("List.list.op #",_) $ _ $ Const("List.list.[]",_)) = true
    1.15 +fun list1 (Const("List.list.Cons",_) $ _ $ Const("List.list.Nil",_)) = true
    1.16    | list1 _ = false;
    1.17  
    1.18 -fun butlast ((cons as Const("List.list.op #",_) $ x) $ xs) =
    1.19 -      (case xs of Const("List.list.[]",_) => xs | _ => cons $ butlast xs)
    1.20 +fun butlast ((cons as Const("List.list.Cons",_) $ x) $ xs) =
    1.21 +      (case xs of Const("List.list.Nil",_) => xs | _ => cons $ butlast xs)
    1.22    | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
    1.23 -  | butlast xs = Const("List.list.[]",fastype_of xs);
    1.24 +  | butlast xs = Const("List.list.Nil",fastype_of xs);
    1.25  
    1.26  val rearr_tac =
    1.27    simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons]);