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.
avoid handle _;
authorwenzelm
Fri, 28 Sep 2001 19:22:40 +0200
changeset 11630 b95f527482fc
parent 11629 481148b273b5
child 11631 b325c05709d3
avoid handle _;
src/HOLCF/adm.ML file | annotate | diff | comparison | revisions 
--- a/src/HOLCF/adm.ML	Fri Sep 28 19:21:26 2001 +0200
+++ b/src/HOLCF/adm.ML	Fri Sep 28 19:22:40 2001 +0200
@@ -104,10 +104,10 @@
          | mk_all ((a,T)::Ts) t = (all T) $ (Abs (a, T, mk_all Ts t));
        val t = HOLogic.mk_Trueprop((Const (cont_name, contT)) $ (Abs(s, T, t)));
        val t' = mk_all params (Logic.list_implies (prems, t));
-       val thm = prove_goalw_cterm [] (cterm_of sign t')
-                  (fn ps => [cut_facts_tac ps 1, tac 1])
+       val thm = transform_error (fn () => prove_goalw_cterm [] (cterm_of sign t')
+                  (fn ps => [cut_facts_tac ps 1, tac 1])) ()
   in (ts, thm)::l end
-  handle _ => l;
+  handle ERROR_MESSAGE _ => l;
 
 
 (*** instantiation of adm_subst theorem (a bit tricky) ***)
isabelle