1.1 --- a/src/Pure/sign.ML	Thu Mar 30 14:18:40 2000 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Mar 30 14:19:13 2000 +0200
     1.3 @@ -90,6 +90,9 @@
     1.4    val infer_types_simult: sg -> (indexname -> typ option) ->
     1.5      (indexname -> sort option) -> string list -> bool
     1.6      -> (xterm list * typ) list -> term list * (indexname * typ) list
     1.7 +  val read_def_terms:
     1.8 +    sg * (indexname -> typ option) * (indexname -> sort option) ->
     1.9 +    string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
    1.10    val add_classes: (bclass * xclass list) list -> sg -> sg
    1.11    val add_classes_i: (bclass * class list) list -> sg -> sg
    1.12    val add_classrel: (xclass * xclass) list -> sg -> sg
    1.13 @@ -670,7 +673,6 @@
    1.14    end;
    1.15  
    1.16  
    1.17 -
    1.18  (** infer_types **)         (*exception ERROR*)
    1.19  
    1.20  (*
    1.21 @@ -728,6 +730,19 @@
    1.22    apfst hd (infer_types_simult sg def_type def_sort used freeze [tsT]);
    1.23  
    1.24  
    1.25 +(** read_def_terms **)
    1.26 +
    1.27 +(*read terms, infer types*)
    1.28 +fun read_def_terms (sign, types, sorts) used freeze sTs =
    1.29 +  let
    1.30 +    val syn = #syn (rep_sg sign);
    1.31 +    fun read (s, T) =
    1.32 +      let val T' = certify_typ sign T handle TYPE (msg, _, _) => error msg
    1.33 +      in (Syntax.read syn T' s, T') end;
    1.34 +    val tsTs = map read sTs;
    1.35 +  in infer_types_simult sign types sorts used freeze tsTs end;
    1.36 +
    1.37 +
    1.38  
    1.39  (** extend signature **)    (*exception ERROR*)
    1.40