# HG changeset patch
# User wenzelm
# Date 878726751 -3600
# Node ID a6ccec4fd0c38c7d14a8b71a0c5d2ab5f52ca3b9
# Parent  e0e5a2820ac108c696b4587e63a80dbacd248f3f
fixed exception OPTION;

diff -r e0e5a2820ac1 -r a6ccec4fd0c3 TFL/tfl.sml
--- a/TFL/tfl.sml	Wed Nov 05 11:43:37 1997 +0100
+++ b/TFL/tfl.sml	Wed Nov 05 11:45:51 1997 +0100
@@ -512,7 +512,7 @@
       val vlist = #2(S.strip_comb (S.rhs body))
       val plist = ListPair.zip (vlist, xlist)
       val args = map (fn qv => the (gen_assoc (op aconv) (plist, qv))) qvars
-                   handle OPTION _ => error 
+                   handle OPTION => error 
                        "TFL fault [alpha_ex_unroll]: no correspondence"
       fun build ex      []   = []
         | build (_$rex) (v::rst) =
diff -r e0e5a2820ac1 -r a6ccec4fd0c3 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Wed Nov 05 11:43:37 1997 +0100
+++ b/src/Provers/blast.ML	Wed Nov 05 11:45:51 1997 +0100
@@ -469,7 +469,7 @@
 fun rot_subgoals_tac [] i st      = Sequence.single st
   | rot_subgoals_tac (k::ks) i st =
       rot_subgoals_tac ks (i+1) (Sequence.hd (rotate_tac (~k) i st))
-      handle OPTION _ => Sequence.null;
+      handle OPTION => Sequence.null;
 
 fun TRACE rl tac st i = if !trace then (prth rl; tac st i) else tac st i;