# HG changeset patch
# User wenzelm
# Date 861904073 -7200
# Node ID 79c1ba7effb25568ca0d38713c97152bff65a536
# Parent  a4b609108712b634bf4c3fedd3440ade54bf9cca
refer to SOME, NONE on top-level;

diff -r a4b609108712 -r 79c1ba7effb2 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Thu Apr 24 19:46:24 1997 +0200
+++ b/src/Provers/blast.ML	Thu Apr 24 19:47:53 1997 +0200
@@ -486,12 +486,12 @@
 	  TRACE rl (etac (if dup then rev_dup_elim rl else rl)) i
 	  THEN rot_subgoals_tac (map nNewHyps (#2 trl)) i
 	  
-  in General.SOME (trl, tac) end
+  in SOME (trl, tac) end
   handle Bind => (*reject: conclusion is not just a variable*)
    (if !trace then (writeln"Warning: ignoring ill-formed elimination rule";
 		    print_thm rl)
     else ();
-    General.NONE);
+    NONE);
 
 
 (*** Conversion of Introduction Rules (needed for efficiency in