Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.

--- a/src/Pure/type.ML	Fri Feb 16 13:29:22 1996 +0100
+++ b/src/Pure/type.ML	Fri Feb 16 13:49:40 1996 +0100
@@ -10,8 +10,9 @@
 *)
 
 signature TYPE =
-sig
-  structure Symtab: SYMTAB
+  sig
+  exception TUNIFY
+  exception TYPE_MATCH
   val no_tvars: typ -> typ
   val varifyT: typ -> typ
   val unvarifyT: typ -> typ
@@ -57,16 +58,11 @@
   val unify: type_sig -> int -> (indexname * typ) list -> (typ * typ)
     -> (indexname * typ) list * int
   val raw_unify: typ * typ -> bool
-  exception TUNIFY
-  exception TYPE_MATCH
-end;
+  end;
 
-functor TypeFun(structure Symtab: SYMTAB and Syntax: SYNTAX): TYPE =
+structure Type : TYPE =
 struct
 
-structure Symtab = Symtab;
-
-
 (*** TFrees vs TVars ***)
 
 (*disallow TVars*)