src/HOLCF/domain/theorems.ML

  (fn prems =>[
                                 resolve_tac prems 1,
                                 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)]);
 (*
 infixr 0 y;
 val b = 0;