diff -r 481148b273b5 -r b95f527482fc src/HOLCF/adm.ML
--- 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) ***)