# HG changeset patch
# User paulson
# Date 860056614 -7200
# Node ID 8d229dc0cfe2755b09671e5d8e6ada6068a8fa93
# Parent  4f2a4c27f9b560f93e383f26c241891c5565cff8
Two extra commands shorten the proof time by 800 seconds...

diff -r 4f2a4c27f9b5 -r 8d229dc0cfe2 src/ZF/Coind/MT.ML
--- a/src/ZF/Coind/MT.ML	Thu Apr 03 10:33:33 1997 +0200
+++ b/src/ZF/Coind/MT.ML	Thu Apr 03 10:36:54 1997 +0200
@@ -57,10 +57,8 @@
 by (rtac ve_owrI 1);
 by clean_tac;
 by (dtac (ElabRel.dom_subset RS subsetD) 1);
-by ( eres_inst_tac 
-     [("Q","te_owr(te,f,t_fun(t1,t2)):TyEnv")] 
-     (SigmaD1 RS te_owrE) 1
-   );
+by (eres_inst_tac [("Q","te_owr(te,f,t_fun(t1,t2)):TyEnv")] 
+    (SigmaD1 RS te_owrE) 1);
 by (assume_tac 1);
 by (rtac ElabRel.elab_fnI 1);
 by clean_tac;
@@ -79,6 +77,8 @@
 by (rtac subsetI 1);
 by (etac RepFunE 1);
 by (excluded_middle_tac "f=y" 1);
+by (rtac UnI1 2);
+by (rtac UnI2 1);
 by (Auto_tac());
 qed "consistency_fix";