src/Pure/axclass.ML

 fun ext_inst_subclass prep_classrel raw_cc tac thy =
   let
     val (c1, c2) = prep_classrel thy raw_cc;
     val txt = quote (Sign.string_of_classrel thy [c1, c2]);
     val _ = message ("Proving class inclusion " ^ txt ^ " ...");
-    val th = Tactic.prove thy [] [] (mk_classrel (c1, c2)) (K tac) handle ERROR =>
-      error ("The error(s) above occurred while trying to prove " ^ txt);
+    val th = Goal.prove thy [] [] (mk_classrel (c1, c2)) (K tac) handle ERROR_MESSAGE msg =>
+      error (msg ^ "\nThe error(s) above occurred while trying to prove " ^ txt);
   in add_classrel_thms [th] thy end;
 
 fun ext_inst_arity prep_arity raw_arity tac thy =
   let
     val arity = prep_arity thy raw_arity;
     val txt = quote (Sign.string_of_arity thy arity);
     val _ = message ("Proving type arity " ^ txt ^ " ...");
     val props = (mk_arities arity);
-    val ths = Tactic.prove_multi thy [] [] props
-        (fn _ => Tactic.smart_conjunction_tac (length props) THEN tac)
-      handle ERROR => error ("The error(s) above occurred while trying to prove " ^ txt);
+    val ths = Goal.prove_multi thy [] [] props
+      (fn _ => Tactic.smart_conjunction_tac (length props) THEN tac) handle ERROR_MESSAGE msg =>
+        error (msg ^ "\nThe error(s) above occurred while trying to prove " ^ txt);
   in add_arity_thms ths thy end;
 
 in
 
 val add_inst_subclass = ext_inst_subclass read_classrel;