--- 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*)