--- a/src/HOL/List.ML Mon Jul 24 23:51:46 2000 +0200
+++ b/src/HOL/List.ML Mon Jul 24 23:52:55 2000 +0200
@@ -238,7 +238,7 @@
local
val list_eq_pattern =
- Thm.read_cterm (Theory.sign_of List.thy) ("(xs::'a list) = ys",HOLogic.boolT);
+ Thm.read_cterm (Theory.sign_of (the_context ())) ("(xs::'a list) = ys",HOLogic.boolT);
fun last (cons as Const("List.list.Cons",_) $ _ $ xs) =
(case xs of Const("List.list.Nil",_) => cons | _ => last xs)
@@ -1490,7 +1490,7 @@
(*** Versions of some theorems above using binary numerals ***)
-AddIffs (map (rename_numerals thy)
+AddIffs (map rename_numerals
[length_0_conv, zero_length_conv, length_greater_0_conv,
sum_eq_0_conv]);