# HG changeset patch
# User wenzelm
# Date 954418753 -7200
# Node ID bf129c6505debc4f9bd82635469b85d54e4fc0d2
# Parent  80992b8566e5afd1890a7dbdd1f71d15ab6858d5
read_def_terms (no certify yet);

diff -r 80992b8566e5 -r bf129c6505de src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Mar 30 14:18:40 2000 +0200
+++ b/src/Pure/sign.ML	Thu Mar 30 14:19:13 2000 +0200
@@ -90,6 +90,9 @@
   val infer_types_simult: sg -> (indexname -> typ option) ->
     (indexname -> sort option) -> string list -> bool
     -> (xterm list * typ) list -> term list * (indexname * typ) list
+  val read_def_terms:
+    sg * (indexname -> typ option) * (indexname -> sort option) ->
+    string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
   val add_classes: (bclass * xclass list) list -> sg -> sg
   val add_classes_i: (bclass * class list) list -> sg -> sg
   val add_classrel: (xclass * xclass) list -> sg -> sg
@@ -670,7 +673,6 @@
   end;
 
 
-
 (** infer_types **)         (*exception ERROR*)
 
 (*
@@ -728,6 +730,19 @@
   apfst hd (infer_types_simult sg def_type def_sort used freeze [tsT]);
 
 
+(** read_def_terms **)
+
+(*read terms, infer types*)
+fun read_def_terms (sign, types, sorts) used freeze sTs =
+  let
+    val syn = #syn (rep_sg sign);
+    fun read (s, T) =
+      let val T' = certify_typ sign T handle TYPE (msg, _, _) => error msg
+      in (Syntax.read syn T' s, T') end;
+    val tsTs = map read sTs;
+  in infer_types_simult sign types sorts used freeze tsTs end;
+
+
 
 (** extend signature **)    (*exception ERROR*)