tuned read_cterms;
authorwenzelm
Mon Oct 06 18:59:49 1997 +0200 (1997-10-06)
changeset 37895802db941718
parent 3788 51bd5c0954c6
child 3790 95a47d8bcd69
tuned read_cterms;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Mon Oct 06 18:57:17 1997 +0200
     1.2 +++ b/src/Pure/thm.ML	Mon Oct 06 18:59:49 1997 +0200
     1.3 @@ -274,21 +274,22 @@
     1.4  (*read a list of terms, matching them against a list of expected types.
     1.5    NO disambiguation of alternative parses via type-checking -- it is just
     1.6    not practical.*)
     1.7 -fun read_cterms sign (bs, Ts) =
     1.8 +fun read_cterms sg (bs, Ts) =
     1.9    let
    1.10 -    val {tsig, syn, ...} = Sign.rep_sg sign;
    1.11 +    val {tsig, syn, ...} = Sign.rep_sg sg;
    1.12      fun read (b, T) =
    1.13        (case Syntax.read syn T b of
    1.14          [t] => t
    1.15        | _  => error ("Error or ambiguity in parsing of " ^ b));
    1.16  
    1.17 -    val prt = setmp Syntax.show_brackets true (Sign.pretty_term sign);
    1.18 -    val prT = Sign.pretty_typ sign;
    1.19 +    val prt = setmp Syntax.show_brackets true (Sign.pretty_term sg);
    1.20 +    val prT = Sign.pretty_typ sg;
    1.21      val (us, _) =
    1.22 -      Type.infer_types prt prT tsig (Sign.const_type sign)
    1.23 -        (K None) (K None) [] true (map (Sign.certify_typ sign) Ts)
    1.24 -        (ListPair.map read (bs, Ts));
    1.25 -  in map (cterm_of sign) us end
    1.26 +      (* FIXME Sign.infer_types!? *)
    1.27 +      Type.infer_types prt prT tsig (Sign.const_type sg) (K None) (K None)
    1.28 +        (Sign.intern_const sg) (Sign.intern_tycons sg) (Sign.intern_sort sg)
    1.29 +        [] true (map (Sign.certify_typ sg) Ts) (ListPair.map read (bs, Ts));
    1.30 +  in map (cterm_of sg) us end
    1.31    handle TYPE (msg, _, _) => error msg
    1.32         | TERM (msg, _) => error msg;
    1.33