src/HOL/List.ML
changeset 9423 7aa79267fa82
parent 9336 9ae89b9ce206
child 9639 51107e8149a0
     1.1 --- a/src/HOL/List.ML	Mon Jul 24 23:51:46 2000 +0200
     1.2 +++ b/src/HOL/List.ML	Mon Jul 24 23:52:55 2000 +0200
     1.3 @@ -238,7 +238,7 @@
     1.4  local
     1.5  
     1.6  val list_eq_pattern =
     1.7 -  Thm.read_cterm (Theory.sign_of List.thy) ("(xs::'a list) = ys",HOLogic.boolT);
     1.8 +  Thm.read_cterm (Theory.sign_of (the_context ())) ("(xs::'a list) = ys",HOLogic.boolT);
     1.9  
    1.10  fun last (cons as Const("List.list.Cons",_) $ _ $ xs) =
    1.11        (case xs of Const("List.list.Nil",_) => cons | _ => last xs)
    1.12 @@ -1490,7 +1490,7 @@
    1.13  
    1.14  (*** Versions of some theorems above using binary numerals ***)
    1.15  
    1.16 -AddIffs (map (rename_numerals thy) 
    1.17 +AddIffs (map rename_numerals
    1.18  	  [length_0_conv, zero_length_conv, length_greater_0_conv,
    1.19  	   sum_eq_0_conv]);
    1.20