Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed exception OPTION;
authorwenzelm
Wed, 05 Nov 1997 11:45:51 +0100
changeset 4149 a6ccec4fd0c3
parent 4148 e0e5a2820ac1
child 4150 56025371fc02
fixed exception OPTION;
TFL/tfl.sml file | annotate | diff | comparison | revisions
src/Provers/blast.ML file | annotate | diff | comparison | revisions 
--- 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) =
--- 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;
isabelle