src/Pure/axclass.ML
changeset 18678 dd0c569fa43d
parent 18574 46ed84a64cf6
child 18708 4b3dadb4fe33
     1.1 --- a/src/Pure/axclass.ML	Fri Jan 13 17:39:41 2006 +0100
     1.2 +++ b/src/Pure/axclass.ML	Sat Jan 14 17:14:06 2006 +0100
     1.3 @@ -274,8 +274,8 @@
     1.4      val (c1, c2) = prep_classrel thy raw_cc;
     1.5      val txt = quote (Sign.string_of_classrel thy [c1, c2]);
     1.6      val _ = message ("Proving class inclusion " ^ txt ^ " ...");
     1.7 -    val th = Goal.prove thy [] [] (mk_classrel (c1, c2)) (K tac) handle ERROR_MESSAGE msg =>
     1.8 -      error (msg ^ "\nThe error(s) above occurred while trying to prove " ^ txt);
     1.9 +    val th = Goal.prove thy [] [] (mk_classrel (c1, c2)) (K tac) handle ERROR msg =>
    1.10 +      cat_error msg ("The error(s) above occurred while trying to prove " ^ txt);
    1.11    in add_classrel_thms [th] thy end;
    1.12  
    1.13  fun ext_inst_arity prep_arity raw_arity tac thy =
    1.14 @@ -285,9 +285,8 @@
    1.15      val _ = message ("Proving type arity " ^ txt ^ " ...");
    1.16      val props = (mk_arities arity);
    1.17      val ths = Goal.prove_multi thy [] [] props
    1.18 -      (fn _ => Tactic.precise_conjunction_tac (length props) 1 THEN tac)
    1.19 -        handle ERROR_MESSAGE msg =>
    1.20 -          error (msg ^ "\nThe error(s) above occurred while trying to prove " ^ txt);
    1.21 +      (fn _ => Tactic.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg =>
    1.22 +        cat_error msg ("\nThe error(s) above occurred while trying to prove " ^ txt);
    1.23    in add_arity_thms ths thy end;
    1.24  
    1.25  in