1.1 --- a/src/HOL/UNITY/Union.ML	Tue Nov 30 16:54:10 1999 +0100
     1.2 +++ b/src/HOL/UNITY/Union.ML	Tue Nov 30 17:53:34 1999 +0100
     1.3 @@ -371,12 +371,6 @@
     1.4  				  Join_left_absorb]) 1);
     1.5  qed "self_Join_LocalTo";
     1.6  
     1.7 -Goalw [LOCALTO_def]
     1.8 -     "[| G : v localTo[C] F;  F<=F' |] ==> G : v localTo[C] F'";
     1.9 -by (Force_tac 1);
    1.10 -qed "localTo_imp_o_localTo";
    1.11 -
    1.12 -
    1.13  
    1.14  (*** Higher-level rules involving localTo and Join ***)
    1.15