# HG changeset patch
# User wenzelm
# Date 1130939211 -3600
# Node ID ad97e231bf8aecf1578f39c82a44a6a0a3179500
# Parent  397b39b06ec8b33d1793a9266e78c505f3904ecb
dist_eqI: the_context();

diff -r 397b39b06ec8 -r ad97e231bf8a src/HOLCF/domain/theorems.ML
--- 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)]);
 (*