src/Pure/sign.ML
changeset 14993 802f3732a54e
parent 14987 699239c7632c
child 15531 08c8dad8e399
     1.1 --- a/src/Pure/sign.ML	Tue Jun 22 09:51:23 2004 +0200
     1.2 +++ b/src/Pure/sign.ML	Tue Jun 22 09:51:39 2004 +0200
     1.3 @@ -671,8 +671,8 @@
     1.4  (*read and certify typ wrt a signature*)
     1.5  local
     1.6    fun read_typ_aux rd cert (sg, def_sort) str =
     1.7 -    (#1 (cert (tsig_of sg) (rd (sg, def_sort) str))
     1.8 -      handle TYPE (msg, _, _) => (error_msg msg; err_in_type str));
     1.9 +    cert (tsig_of sg) (rd (sg, def_sort) str)
    1.10 +      handle TYPE (msg, _, _) => (error_msg msg; err_in_type str);
    1.11  in
    1.12    val read_typ          = read_typ_aux read_raw_typ Type.cert_typ;
    1.13    val read_typ_raw      = read_typ_aux read_raw_typ Type.cert_typ_raw;
    1.14 @@ -686,8 +686,8 @@
    1.15  
    1.16  val certify_class = Type.cert_class o tsig_of;
    1.17  val certify_sort = Type.cert_sort o tsig_of;
    1.18 -val certify_typ = #1 oo (Type.cert_typ o tsig_of);
    1.19 -val certify_typ_raw = #1 oo (Type.cert_typ_raw o tsig_of);
    1.20 +val certify_typ = Type.cert_typ o tsig_of;
    1.21 +val certify_typ_raw = Type.cert_typ_raw o tsig_of;
    1.22  
    1.23  fun certify_tyname sg c =
    1.24    if is_some (Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c)) then c
    1.25 @@ -702,22 +702,6 @@
    1.26  
    1.27  local
    1.28  
    1.29 -(*certify types of term and compute maxidx*)
    1.30 -fun cert_term_types certT =
    1.31 -  let
    1.32 -    fun cert (Const (a, T)) = let val (T', i) = certT T in (Const (a, T'), i) end
    1.33 -      | cert (Free (a, T)) = let val (T', i) = certT T in (Free (a, T'), i) end
    1.34 -      | cert (Var (xi as (_, i), T)) =
    1.35 -          let val (T', j) = certT T in (Var (xi, T'), Int.max (i, j)) end
    1.36 -      | cert (t as Bound _) = (t, ~1)
    1.37 -      | cert (Abs (a, T, t)) =
    1.38 -          let val (T', i) = certT T and (t', j) = cert t
    1.39 -          in (Abs (a, T', t'), Int.max (i, j)) end
    1.40 -      | cert (t $ u) =
    1.41 -          let val (t', i) = cert t and (u', j) =  cert u
    1.42 -          in (t' $ u', Int.max (i, j)) end;
    1.43 -  in cert end;
    1.44 -
    1.45  (*compute and check type of the term*)
    1.46  fun type_check pp sg tm =
    1.47    let
    1.48 @@ -797,7 +781,7 @@
    1.49    let
    1.50      val _ = check_stale sg;
    1.51  
    1.52 -    val (tm', maxidx) = cert_term_types (Type.cert_typ (tsig_of sg)) tm;
    1.53 +    val tm' = map_term_types (Type.cert_typ (tsig_of sg)) tm;
    1.54      val tm' = if tm = tm' then tm else tm';  (*avoid copying of already normal term*)
    1.55  
    1.56      fun err msg = raise TYPE (msg, [], [tm']);
    1.57 @@ -818,7 +802,7 @@
    1.58    in
    1.59      check_atoms tm';
    1.60      nodup_vars tm';
    1.61 -    (tm', type_check pp sg tm', maxidx)
    1.62 +    (tm', type_check pp sg tm', maxidx_of_term tm')
    1.63    end;
    1.64  
    1.65  end;
    1.66 @@ -1001,8 +985,7 @@
    1.67      raw_consts =
    1.68    let
    1.69      val prep_typ = compress_type o Type.varifyT o Type.no_tvars o
    1.70 -     (if syn_only then #1 o Type.cert_typ_syntax tsig
    1.71 -      else Term.no_dummyT o #1 o Type.cert_typ tsig);
    1.72 +     (if syn_only then Type.cert_typ_syntax tsig else Term.no_dummyT o Type.cert_typ tsig);
    1.73      fun prep_const (c, ty, mx) = (c, prep_typ ty, mx) handle TYPE (msg, _, _) =>
    1.74        (error_msg msg; err_in_const (const_name path c mx));
    1.75