src/HOL/Tools/typedef_package.ML
changeset 18678 dd0c569fa43d
parent 18643 89a7978f90e1
child 18708 4b3dadb4fe33
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Fri Jan 13 17:39:41 2006 +0100
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Sat Jan 14 17:14:06 2006 +0100
     1.3 @@ -93,8 +93,8 @@
     1.4  
     1.5  fun cert_term thy _ t = Thm.cterm_of thy t handle TERM (msg, _) => error msg;
     1.6  
     1.7 -fun err_in_typedef name =
     1.8 -  error ("The error(s) above occurred in typedef " ^ quote name);
     1.9 +fun err_in_typedef msg name =
    1.10 +  cat_error msg ("The error(s) above occurred in typedef " ^ quote name);
    1.11  
    1.12  fun prepare_typedef prep_term def name (t, vs, mx) raw_set opt_morphs thy =
    1.13    let
    1.14 @@ -224,7 +224,7 @@
    1.15        setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal) |> typedef_result;
    1.16  
    1.17    in (cset, goal, goal_pat, typedef_result) end
    1.18 -  handle ERROR => err_in_typedef name;
    1.19 +  handle ERROR msg => err_in_typedef msg name;
    1.20  
    1.21  
    1.22  (* add_typedef interfaces *)
    1.23 @@ -237,8 +237,8 @@
    1.24      val (cset, goal, _, typedef_result) =
    1.25        prepare_typedef prep_term def name typ set opt_morphs thy;
    1.26      val _ = message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ...");
    1.27 -    val non_empty = Goal.prove thy [] [] goal (K tac) handle ERROR_MESSAGE msg =>
    1.28 -      error (msg ^ "\nFailed to prove non-emptiness of " ^ quote (string_of_cterm cset));
    1.29 +    val non_empty = Goal.prove thy [] [] goal (K tac) handle ERROR msg =>
    1.30 +      cat_error msg ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset));
    1.31      val ((thy', _), result) = (thy, non_empty) |> typedef_result;
    1.32    in (thy', result) end;
    1.33