# HG changeset patch
# User wenzelm
# Date 964475575 -7200
# Node ID 7aa79267fa82bb74567fc12e01f4ca65ef4286e0
# Parent  4b6bc2b347e5aa72bca892293a3a404956e5b46f
avoid referencing thy value;
rename_numerals: use implicit theory context;

diff -r 4b6bc2b347e5 -r 7aa79267fa82 src/HOL/List.ML
--- 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]);