refer to SOME, NONE on top-level;
authorwenzelm
Thu, 24 Apr 1997 19:47:53 +0200
changeset 3049 79c1ba7effb2
parent 3048 a4b609108712
child 3050 7eacab79b8e1
refer to SOME, NONE on top-level;
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