src/Pure/section_utils.ML
changeset 1390 bf523422a3df
parent 654 65435e2c6512
child 1458 fd510875fb71
     1.1 --- a/src/Pure/section_utils.ML	Thu Dec 07 18:36:33 1995 +0100
     1.2 +++ b/src/Pure/section_utils.ML	Fri Dec 08 10:23:29 1995 +0100
     1.3 @@ -24,9 +24,10 @@
     1.4  (*Read an assumption in the given theory*)
     1.5  fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
     1.6  
     1.7 -fun readtm sign T a = 
     1.8 -    read_cterm sign (a,T) |> term_of
     1.9 -    handle ERROR => error ("The error above occurred for " ^ a);
    1.10 +(*Read a term from string "b", with expected type T*)
    1.11 +fun readtm sign T b = 
    1.12 +    read_cterm sign (b,T) |> term_of
    1.13 +    handle ERROR => error ("The error above occurred for " ^ b);
    1.14  
    1.15  (*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
    1.16  fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))