src/Pure/theory.ML
changeset 18678 dd0c569fa43d
parent 18338 ed2d0e60fbcc
child 18763 e2b4ba340ff1
     1.1 --- a/src/Pure/theory.ML	Fri Jan 13 17:39:41 2006 +0100
     1.2 +++ b/src/Pure/theory.ML	Sat Jan 14 17:14:06 2006 +0100
     1.3 @@ -163,8 +163,8 @@
     1.4  
     1.5  (* prepare axioms *)
     1.6  
     1.7 -fun err_in_axm name =
     1.8 -  error ("The error(s) above occurred in axiom " ^ quote name);
     1.9 +fun err_in_axm msg name =
    1.10 +  cat_error msg ("The error(s) above occurred in axiom " ^ quote name);
    1.11  
    1.12  fun no_vars pp tm =
    1.13    (case (Term.term_vars tm, Term.term_tvars tm) of
    1.14 @@ -190,7 +190,7 @@
    1.15      val ts = Syntax.read thy (Sign.is_logtype thy) (Sign.syn_of thy) propT str;
    1.16      val (t, _) = Sign.infer_types (Sign.pp thy) thy types sorts used true (ts, propT);
    1.17    in cert_axm thy (name, t) end
    1.18 -  handle ERROR => err_in_axm name;
    1.19 +  handle ERROR msg => err_in_axm msg name;
    1.20  
    1.21  fun read_axm thy name_str = read_def_axm (thy, K NONE, K NONE) [] name_str;
    1.22  
    1.23 @@ -199,7 +199,7 @@
    1.24      val pp = Sign.pp thy;
    1.25      val (t, _) = Sign.infer_types pp thy (K NONE) (K NONE) [] true ([pre_tm], propT);
    1.26    in (name, no_vars pp t) end
    1.27 -  handle ERROR => err_in_axm name;
    1.28 +  handle ERROR msg => err_in_axm msg name;
    1.29  
    1.30  
    1.31  (* add_axioms(_i) *)
    1.32 @@ -309,7 +309,7 @@
    1.33      defs |> Defs.define (Sign.the_const_type thy)
    1.34        name (prep_const thy const) (map (prep_const thy) rhs_consts)
    1.35    end
    1.36 -  handle ERROR => error (Pretty.string_of (Pretty.block
    1.37 +  handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
    1.38     [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"),
    1.39      Pretty.fbrk, Pretty.quote (Pretty.term (Sign.pp thy) tm)]));
    1.40