dist_eqI: the_context();

--- a/src/HOLCF/domain/theorems.ML	Wed Nov 02 14:46:49 2005 +0100
+++ b/src/HOLCF/domain/theorems.ML	Wed Nov 02 14:46:51 2005 +0100
@@ -45,7 +45,7 @@
                                 cut_facts_tac prems 1,
                                 fast_tac HOL_cs 1]);
 
-val dist_eqI = prove_goal Porder.thy "!!x::'a::po. ~ x << y ==> x ~= y" 
+val dist_eqI = prove_goal (the_context ()) "!!x::'a::po. ~ x << y ==> x ~= y" 
              (fn prems => [
                (blast_tac (claset() addDs [antisym_less_inverse]) 1)]);
 (*