src/Pure/section_utils.ML
changeset 3536 8fb4150e2ad3
parent 2863 d97f5f424b97
child 3934 a9c8960e4da6
     1.1 --- a/src/Pure/section_utils.ML	Fri Jul 18 13:57:19 1997 +0200
     1.2 +++ b/src/Pure/section_utils.ML	Fri Jul 18 14:06:54 1997 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4  (*Read a term from string "b", with expected type T*)
     1.5  fun readtm sign T b = 
     1.6      read_cterm sign (b,T) |> term_of
     1.7 -    handle ERROR => error ("The error above occurred for " ^ b);
     1.8 +    handle ERROR => error ("The error(s) above occurred for " ^ b);
     1.9  
    1.10  (*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
    1.11  fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))