4848

1 
(* Title: Pure/section_utils.ML

579

2 
ID: $Id$

1460

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

579

4 
Copyright 1994 University of Cambridge


5 

4848

6 
Utilities for writing new theory sections.

579

7 
*)


8 


9 
fun ap t u = t$u;


10 
fun app t (u1,u2) = t $ u1 $ u2;


11 


12 
(*Make distinct individual variables a1, a2, a3, ..., an. *)


13 
fun mk_frees a [] = []


14 
 mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;


15 


16 


17 
(*Read an assumption in the given theory*)

4848

18 
fun assume_read thy a = Thm.assume (read_cterm (sign_of thy) (a,propT));

579

19 

1390

20 
(*Read a term from string "b", with expected type T*)


21 
fun readtm sign T b =


22 
read_cterm sign (b,T) > term_of

3536

23 
handle ERROR => error ("The error(s) above occurred for " ^ b);

579

24 


25 
(*From HOL/ex/meson.ML: raises exception if no rules apply  unlike RL*)


26 
fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))


27 
 tryres (th, []) = raise THM("tryres", 0, [th]);


28 


29 
fun gen_make_elim elim_rls rl =


30 
standard (tryres (rl, elim_rls @ [revcut_rl]));


31 


32 
(** String manipulation **)


33 

4695

34 
(*Skipping initial blanks, find the first identifier*) (* FIXME *)

579

35 
fun scan_to_id s =

4695

36 
s > Symbol.explode

4938

37 
> Scan.error (Scan.finite Symbol.stopper

4695

38 
(!! (fn _ => "Expected to find an identifier in " ^ s)


39 
(Scan.any Symbol.is_blank  Syntax.scan_id)))


40 
> #1;

579

41 


42 
fun is_backslash c = c = "\\";
