# HG changeset patch
# User paulson
# Date 878385603 -3600
# Node ID 600f266eac454e82daf0f347ec61c8c1bffe5070
# Parent  59c1422c9da5fd037446231af25de4fe37df0eb7
Set.thy was too specific

diff -r 59c1422c9da5 -r 600f266eac45 src/HOL/Subst/Subst.ML
--- a/src/HOL/Subst/Subst.ML	Sat Nov 01 12:59:06 1997 +0100
+++ b/src/HOL/Subst/Subst.ML	Sat Nov 01 13:00:03 1997 +0100
@@ -153,7 +153,7 @@
 by (Blast_tac 1);
 qed "srange_iff";
 
-goalw Set.thy [empty_def] "(A = {}) = (ALL a.~ a:A)";
+goalw thy [empty_def] "(A = {}) = (ALL a.~ a:A)";
 by (Blast_tac 1);
 qed "empty_iff_all_not";