src/Pure/thm.ML
changeset 4315 f4bc2f6ee5e0
parent 4288 3f5e8c4aa84d
child 4397 7f760385a3a5
     1.1 --- a/src/Pure/thm.ML	Thu Nov 27 19:36:31 1997 +0100
     1.2 +++ b/src/Pure/thm.ML	Thu Nov 27 19:36:51 1997 +0100
     1.3 @@ -288,31 +288,6 @@
     1.4  
     1.5  fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None) [] true;
     1.6  
     1.7 -(*read a list of terms, matching them against a list of expected types.
     1.8 -  NO disambiguation of alternative parses via type-checking -- it is just
     1.9 -  not practical.
    1.10 -
    1.11 -Why not? In any case, this function is not used at all.
    1.12 -
    1.13 -fun read_cterms sg (bs, Ts) =
    1.14 -  let
    1.15 -    val {tsig, syn, ...} = Sign.rep_sg sg;
    1.16 -    fun read (b, T) =
    1.17 -      (case Syntax.read syn T b of
    1.18 -        [t] => t
    1.19 -      | _  => error ("Error or ambiguity in parsing of " ^ b));
    1.20 -
    1.21 -    val prt = setmp Syntax.show_brackets true (Sign.pretty_term sg);
    1.22 -    val prT = Sign.pretty_typ sg;
    1.23 -    val (us, _) =
    1.24 -      (* FIXME Sign.infer_types!? *)
    1.25 -      Type.infer_types prt prT tsig (Sign.const_type sg) (K None) (K None)
    1.26 -        (Sign.intern_const sg) (Sign.intern_tycons sg) (Sign.intern_sort sg)
    1.27 -        [] true (map (Sign.certify_typ sg) Ts) (ListPair.map read (bs, Ts));
    1.28 -  in map (cterm_of sg) us end
    1.29 -  handle TYPE (msg, _, _) => error msg
    1.30 -       | TERM (msg, _) => error msg;
    1.31 -*)
    1.32  
    1.33  
    1.34  (*** Derivations ***)