# HG changeset patch
# User paulson
# Date 824477929 -3600
# Node ID 20d9811f1fd1c10d73c99352f285162ee1a8ea9d
# Parent  f600215b6ea775d73ebab5dfdb386d96e300dd03
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.

diff -r f600215b6ea7 -r 20d9811f1fd1 src/Pure/Syntax/pretty.ML
--- 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*)