src/Pure/goal.ML
changeset 18678 dd0c569fa43d
parent 18497 7569674d7bb1
child 19184 3e30297e1300
     1.1 --- a/src/Pure/goal.ML	Fri Jan 13 17:39:41 2006 +0100
     1.2 +++ b/src/Pure/goal.ML	Sat Jan 14 17:14:06 2006 +0100
     1.3 @@ -123,8 +123,8 @@
     1.4      val fixed_tfrees = fold (Term.add_tfreesT o #2) fixed_frees [];
     1.5      val params = List.mapPartial (fn x => Option.map (pair x) (AList.lookup (op =) frees x)) xs;
     1.6  
     1.7 -    fun err msg = raise ERROR_MESSAGE
     1.8 -      (msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^
     1.9 +    fun err msg = cat_error msg
    1.10 +      ("The error(s) above occurred for the goal statement:\n" ^
    1.11          Sign.string_of_term thy (Term.list_all_free (params, statement)));
    1.12  
    1.13      fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm t)
    1.14 @@ -165,7 +165,7 @@
    1.15  fun prove_raw casms cprop tac =
    1.16    (case SINGLE (tac (map (norm_hhf o Thm.assume) casms)) (init cprop) of
    1.17      SOME th => Drule.implies_intr_list casms (finish th)
    1.18 -  | NONE => raise ERROR_MESSAGE "Tactic failed.");
    1.19 +  | NONE => error "Tactic failed.");
    1.20  
    1.21  
    1.22  (* SELECT_GOAL *)