diff -r 01fdd1ea6324 -r b2de3b3277b8 src/Pure/net.ML
--- a/src/Pure/net.ML	Fri Feb 16 12:08:49 1996 +0100
+++ b/src/Pure/net.ML	Fri Feb 16 12:19:47 1996 +0100
@@ -31,7 +31,7 @@
   end;
 
 
-functor NetFun () : NET = 
+structure Net : NET = 
 struct
 
 datatype key = CombK | VarK | AtomK of string;