diff -r eec3a9222b50 -r 653b752e2ddb src/Pure/type.ML
--- a/src/Pure/type.ML	Fri Aug 19 15:41:39 1994 +0200
+++ b/src/Pure/type.ML	Fri Aug 19 15:42:13 1994 +0200
@@ -41,7 +41,7 @@
   val norm_typ: type_sig -> typ -> typ
   val freeze: (indexname -> bool) -> term -> term
   val freeze_vars: typ -> typ
-  val infer_types: type_sig * typ Symtab.table * (indexname -> typ option) *
+  val infer_types: type_sig * (string -> typ option) * (indexname -> typ option) *
     (indexname -> sort option) * typ * term -> term * (indexname * typ) list
   val inst_term_tvars: type_sig * (indexname * typ) list -> term -> term
   val thaw_vars: typ -> typ
@@ -80,9 +80,9 @@
 (* print sorts and arities *)
 
 fun str_of_sort [c] = c
-  | str_of_sort cs = parents "{" "}" (commas cs);
+  | str_of_sort cs = enclose "{" "}" (commas cs);
 
-fun str_of_dom dom = parents "(" ")" (commas (map str_of_sort dom));
+fun str_of_dom dom = enclose "(" ")" (commas (map str_of_sort dom));
 
 fun str_of_arity (t, [], S) = t ^ " :: " ^ str_of_sort S
   | str_of_arity (t, SS, S) =
@@ -769,7 +769,7 @@
 them apart from normal TVars, which is essential, because at the end the type
 of the term is unified with the expected type, which contains normal TVars.
 
-1. Add initial type information to the term (add_types).
+1. Add initial type information to the term (attach_types).
    This freezes (freeze_vars) TVars in explicitly provided types (eg
    constraints or defaults) by turning them into TFrees.
 2. Carry out type inference, possibly introducing new negative TVars.
@@ -912,12 +912,16 @@
   to get consistent typing.*)
 fun new_id_type a = TVar(("'"^a, new_tvar_inx()), []);
 fun type_of_ixn(types, ixn as (a, _)) =
-        case types ixn of Some T => freeze_vars T | None => TVar(("'"^a, ~1), []);
+  case types ixn of Some T => freeze_vars T | None => TVar(("'"^a, ~1), []);
+
+fun constrain (term, T) = Const (Syntax.constrainC, T --> T) $ term;
 
-fun constrain(term, T) = Const(Syntax.constrainC, T-->T) $ term;
-fun constrainAbs(Abs(a, _, body), T) = Abs(a, T, body);
+fun constrainAbs (Abs (a, _, body), T) = Abs (a, T, body)
+  | constrainAbs _ = sys_error "constrainAbs";
 
 
+(* attach_types *)
+
 (*
   Attach types to a term. Input is a "parse tree" containing dummy types.
   Type constraints are translated and checked for validity wrt tsig. TVars in
@@ -939,27 +943,28 @@
     bound variables of the same name but different types.
 *)
 
-(* FIXME replace const_tab by (const_typ: string -> typ option) (?) *)
-(* FIXME improve handling of sort constraints *)
+(* FIXME consitency of sort_env / sorts (!?) *)
 
-fun add_types (tsig, const_tab, types, sorts) =
+(* FIXME check *)
+
+fun attach_types (tsig, const_type, types, sorts) tm =
   let
-    val S0 = defaultS tsig;
-    fun defS0 ixn = if_none (sorts ixn) S0;
+    val sort_env = Syntax.raw_term_sorts tm;
+    fun def_sort xi = if_none (sorts xi) (defaultS tsig);
 
-    fun prepareT typ =
-      freeze_vars (cert_typ tsig (Syntax.typ_of_term defS0 typ));
+    fun prepareT t =
+      freeze_vars (cert_typ tsig (Syntax.typ_of_term sort_env def_sort t));
 
     fun add (Const (a, _)) =
-          (case Symtab.lookup (const_tab, a) of
+          (case const_type a of
             Some T => type_const (a, T)
           | None => raise_type ("No such constant: " ^ quote a) [] [])
-      | add (Bound i) = Bound i
       | add (Free (a, _)) =
-          (case Symtab.lookup (const_tab, a) of
+          (case const_type a of
             Some T => type_const (a, T)
           | None => Free (a, type_of_ixn (types, (a, ~1))))
       | add (Var (ixn, _)) = Var (ixn, type_of_ixn (types, ixn))
+      | add (Bound i) = Bound i
       | add (Abs (a, _, body)) = Abs (a, new_id_type a, add body)
       | add ((f as Const (a, _) $ t1) $ t2) =
           if a = Syntax.constrainC then
@@ -968,12 +973,11 @@
             constrainAbs (add t1, prepareT t2)
           else add f $ add t2
       | add (f $ t) = add f $ add t;
-  in add end;
+  in add tm end;
 
 
 (* Post-Processing *)
 
-
 (*Instantiation of type variables in terms*)
 fun inst_types tye = map_term_types (inst_typ tye);
 
@@ -1014,20 +1018,23 @@
 
 (*Infer types for term t using tables. Check that t's type and T unify *)
 
-fun infer_term (tsig, const_tab, types, sorts, T, t) =
-  let val u = add_types (tsig, const_tab, types, sorts) t;
-      val (U, tye) = infer tsig ([], u, []);
-      val uu = unconstrain u;
-      val tye' = unify tsig ((T, U), tye) handle TUNIFY => raise TYPE
-        ("Term does not have expected type", [T, U], [inst_types tye uu])
-      val Ttye = restrict tye' (* restriction to TVars in T *)
-      val all = Const("", Type("", map snd Ttye)) $ (inst_types tye' uu)
-        (* all is a dummy term which contains all exported TVars *)
-      val Const(_, Type(_, Ts)) $ u'' =
-            map_term_types thaw_vars (freeze (fn (_, i) => i<0) all)
-        (* turn all internally generated TVars into TFrees
-           and thaw all initially frozen TVars *)
-  in (u'', (map fst Ttye) ~~ Ts) end;
+fun infer_term (tsig, const_type, types, sorts, T, t) =
+  let
+    val u = attach_types (tsig, const_type, types, sorts) t;
+    val (U, tye) = infer tsig ([], u, []);
+    val uu = unconstrain u;
+    val tye' = unify tsig ((T, U), tye) handle TUNIFY => raise TYPE
+      ("Term does not have expected type", [T, U], [inst_types tye uu])
+    val Ttye = restrict tye' (*restriction to TVars in T*)
+    val all = Const("", Type("", map snd Ttye)) $ (inst_types tye' uu)
+      (*all is a dummy term which contains all exported TVars*)
+    val Const(_, Type(_, Ts)) $ u'' =
+      map_term_types thaw_vars (freeze (fn (_, i) => i < 0) all)
+      (*turn all internally generated TVars into TFrees
+        and thaw all initially frozen TVars*)
+  in
+    (u'', (map fst Ttye) ~~ Ts)
+  end;
 
 fun infer_types args = (tyinit(); infer_term args);