tuned error propagation msg;
authorwenzelm
Fri Jul 18 14:06:54 1997 +0200 (1997-07-18)
changeset 35368fb4150e2ad3
parent 3535 19bd6c8274c4
child 3537 79ac9b475621
tuned error propagation msg;
src/Pure/goals.ML
src/Pure/section_utils.ML
     1.1 --- a/src/Pure/goals.ML	Fri Jul 18 13:57:19 1997 +0200
     1.2 +++ b/src/Pure/goals.ML	Fri Jul 18 14:06:54 1997 +0200
     1.3 @@ -215,7 +215,7 @@
     1.4        val chorn = read_cterm sign (agoal,propT)
     1.5    in  prove_goalw_cterm rths chorn tacsf end
     1.6    handle ERROR => error (*from read_cterm?*)
     1.7 -		("The error above occurred for " ^ quote agoal);
     1.8 +		("The error(s) above occurred for " ^ quote agoal);
     1.9  
    1.10  (*String version with no meta-rewrite-rules*)
    1.11  fun prove_goal thy = prove_goalw thy [];
    1.12 @@ -318,7 +318,7 @@
    1.13  fun goalw thy rths agoal = 
    1.14    goalw_cterm rths (read_cterm(sign_of thy)(agoal,propT))
    1.15    handle ERROR => error (*from type_assign, etc via prepare_proof*)
    1.16 -	    ("The error above occurred for " ^ quote agoal);
    1.17 +	    ("The error(s) above occurred for " ^ quote agoal);
    1.18  
    1.19  (*String version with no meta-rewrite-rules*)
    1.20  fun goal thy = goalw thy [];
     2.1 --- a/src/Pure/section_utils.ML	Fri Jul 18 13:57:19 1997 +0200
     2.2 +++ b/src/Pure/section_utils.ML	Fri Jul 18 14:06:54 1997 +0200
     2.3 @@ -27,7 +27,7 @@
     2.4  (*Read a term from string "b", with expected type T*)
     2.5  fun readtm sign T b = 
     2.6      read_cterm sign (b,T) |> term_of
     2.7 -    handle ERROR => error ("The error above occurred for " ^ b);
     2.8 +    handle ERROR => error ("The error(s) above occurred for " ^ b);
     2.9  
    2.10  (*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
    2.11  fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))