diff -r 18e993700540 -r f381c1a98209 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Nov 26 16:15:50 1996 +0100
+++ b/src/Pure/sign.ML	Tue Nov 26 16:18:42 1996 +0100
@@ -151,7 +151,7 @@
 
 (** print signature **)
 
-val stamp_names = rev o map !;
+fun stamp_names stamps = rev (map ! stamps);
 
 fun print_sg sg =
   let
@@ -424,8 +424,8 @@
     (syn1, Type.ext_tsig_abbrs tsig (map decl_of abbrs), ctab)
   end;
 
-val ext_tyabbrs_i = ext_abbrs (K (K I));
-val ext_tyabbrs = ext_abbrs read_abbr;
+fun ext_tyabbrs_i arg = ext_abbrs (K (K I)) arg;
+fun ext_tyabbrs   arg = ext_abbrs read_abbr arg;
 
 
 (* add type arities *)