src/HOL/List.ML
changeset 6394 3d9fd50fcc43
parent 6306 81e7fbf61db2
child 6408 5b443d6331ed
     1.1 --- a/src/HOL/List.ML	Wed Mar 17 16:53:32 1999 +0100
     1.2 +++ b/src/HOL/List.ML	Wed Mar 17 16:53:46 1999 +0100
     1.3 @@ -251,7 +251,7 @@
     1.4  local
     1.5  
     1.6  val list_eq_pattern =
     1.7 -  read_cterm (sign_of List.thy) ("(xs::'a list) = ys",HOLogic.boolT);
     1.8 +  Thm.read_cterm (Theory.sign_of List.thy) ("(xs::'a list) = ys",HOLogic.boolT);
     1.9  
    1.10  fun last (cons as Const("List.list.op #",_) $ _ $ xs) =
    1.11        (case xs of Const("List.list.[]",_) => cons | _ => last xs)