src/Pure/sign.ML
changeset 8802 2c37263eb903
parent 8730 d97ee7249698
child 8898 a1ee54500516
     1.1 --- a/src/Pure/sign.ML	Fri May 05 21:57:58 2000 +0200
     1.2 +++ b/src/Pure/sign.ML	Fri May 05 21:58:18 2000 +0200
     1.3 @@ -94,6 +94,7 @@
     1.4    val read_def_terms:
     1.5      sg * (indexname -> typ option) * (indexname -> sort option) ->
     1.6      string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
     1.7 +  val simple_read_term: sg -> typ -> string -> term
     1.8    val add_classes: (bclass * xclass list) list -> sg -> sg
     1.9    val add_classes_i: (bclass * class list) list -> sg -> sg
    1.10    val add_classrel: (xclass * xclass) list -> sg -> sg
    1.11 @@ -741,6 +742,10 @@
    1.12      val tsTs = map read sTs;
    1.13    in infer_types_simult sign types sorts used freeze tsTs end;
    1.14  
    1.15 +fun simple_read_term sign T s =
    1.16 +  (read_def_terms (sign, K None, K None) [] true [(s, T)]
    1.17 +    handle ERROR => error ("The error(s) above occurred for " ^ s)) |> #1 |> hd;
    1.18 +
    1.19  
    1.20  
    1.21  (** extend signature **)    (*exception ERROR*)