Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoid referencing thy value;
authorwenzelm
Mon, 24 Jul 2000 23:52:55 +0200
changeset 9423 7aa79267fa82
parent 9422 4b6bc2b347e5
child 9424 234ef8652cae
avoid referencing thy value; rename_numerals: use implicit theory context;
src/HOL/List.ML file | annotate | diff | comparison | revisions 
--- 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]);
isabelle