# HG changeset patch
# User wenzelm
# Date 957556698 -7200
# Node ID 2c37263eb903c574a6fb6f649563f23b3061ec53
# Parent  9d01c9a261345667831c1cbc4a0fbda371bcf160
added simple_read_term;

diff -r 9d01c9a26134 -r 2c37263eb903 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri May 05 21:57:58 2000 +0200
+++ b/src/Pure/sign.ML	Fri May 05 21:58:18 2000 +0200
@@ -94,6 +94,7 @@
   val read_def_terms:
     sg * (indexname -> typ option) * (indexname -> sort option) ->
     string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
+  val simple_read_term: sg -> typ -> string -> term
   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
@@ -741,6 +742,10 @@
     val tsTs = map read sTs;
   in infer_types_simult sign types sorts used freeze tsTs end;
 
+fun simple_read_term sign T s =
+  (read_def_terms (sign, K None, K None) [] true [(s, T)]
+    handle ERROR => error ("The error(s) above occurred for " ^ s)) |> #1 |> hd;
+
 
 
 (** extend signature **)    (*exception ERROR*)