src/Pure/section_utils.ML
author wenzelm
Thu Jul 08 18:31:04 1999 +0200 (1999-07-08)
changeset 6930 4b40fb299f9f
parent 6390 5d58c100ca3f
child 7744 f27d54c1ef39
permissions -rw-r--r--
improved error msgs of cterm_instantiate;
fixed incr_indexes;
wenzelm@4848
     1
(*  Title: 	Pure/section_utils.ML
lcp@579
     2
    ID:         $Id$
clasohm@1460
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@579
     4
    Copyright   1994  University of Cambridge
lcp@579
     5
wenzelm@4848
     6
Utilities for writing new theory sections.
lcp@579
     7
*)
lcp@579
     8
lcp@579
     9
fun ap t u = t$u;
lcp@579
    10
fun app t (u1,u2) = t $ u1 $ u2;
lcp@579
    11
lcp@579
    12
(*Make distinct individual variables a1, a2, a3, ..., an. *)
lcp@579
    13
fun mk_frees a [] = []
lcp@579
    14
  | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;
lcp@579
    15
lcp@579
    16
lcp@579
    17
(*Read an assumption in the given theory*)
wenzelm@6390
    18
fun assume_read thy a = Thm.assume (read_cterm (Theory.sign_of thy) (a,propT));
lcp@579
    19
paulson@1390
    20
(*Read a term from string "b", with expected type T*)
paulson@1390
    21
fun readtm sign T b = 
paulson@1390
    22
    read_cterm sign (b,T) |> term_of
wenzelm@3536
    23
    handle ERROR => error ("The error(s) above occurred for " ^ b);
lcp@579
    24
lcp@579
    25
(*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
lcp@579
    26
fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
lcp@579
    27
  | tryres (th, []) = raise THM("tryres", 0, [th]);
lcp@579
    28
lcp@579
    29
fun gen_make_elim elim_rls rl = 
lcp@579
    30
      standard (tryres (rl, elim_rls @ [revcut_rl]));
lcp@579
    31
lcp@579
    32
(** String manipulation **)
lcp@579
    33
wenzelm@4695
    34
(*Skipping initial blanks, find the first identifier*)	(* FIXME *)
lcp@579
    35
fun scan_to_id s = 
wenzelm@4695
    36
    s |> Symbol.explode
wenzelm@4938
    37
    |> Scan.error (Scan.finite Symbol.stopper
wenzelm@4695
    38
      (!! (fn _ => "Expected to find an identifier in " ^ s)
wenzelm@4695
    39
        (Scan.any Symbol.is_blank |-- Syntax.scan_id)))
wenzelm@4695
    40
    |> #1;
lcp@579
    41
lcp@579
    42
fun is_backslash c = c = "\\";