src/Pure/section_utils.ML
changeset 3536 8fb4150e2ad3
parent 2863 d97f5f424b97
child 3934 a9c8960e4da6
equal deleted inserted replaced
3535:19bd6c8274c4 3536:8fb4150e2ad3
    25 fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
    25 fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
    26 
    26 
    27 (*Read a term from string "b", with expected type T*)
    27 (*Read a term from string "b", with expected type T*)
    28 fun readtm sign T b = 
    28 fun readtm sign T b = 
    29     read_cterm sign (b,T) |> term_of
    29     read_cterm sign (b,T) |> term_of
    30     handle ERROR => error ("The error above occurred for " ^ b);
    30     handle ERROR => error ("The error(s) above occurred for " ^ b);
    31 
    31 
    32 (*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
    32 (*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
    33 fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
    33 fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
    34   | tryres (th, []) = raise THM("tryres", 0, [th]);
    34   | tryres (th, []) = raise THM("tryres", 0, [th]);
    35 
    35