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

--- a/src/Pure/Syntax/pretty.ML	Fri Feb 16 14:17:34 1996 +0100
+++ b/src/Pure/Syntax/pretty.ML	Fri Feb 16 14:38:49 1996 +0100
@@ -24,7 +24,7 @@
   (unit -> unit) * (unit -> unit);
 
 signature PRETTY =
-sig
+  sig
   type T
   val blk: int * T list -> T
   val brk: int -> T
@@ -48,9 +48,9 @@
   val map_strs: (string -> string) -> T -> T
   val setdepth: int -> unit
   val setmargin: int -> unit
-end;
+  end;
 
-functor PrettyFun(): PRETTY =
+structure Pretty : PRETTY =
 struct
 
 (*Printing items: compound phrases, strings, and breaks*)