diff -r 29bda008409e -r 30a4267c6301 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Apr 26 16:31:43 2005 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Apr 26 17:44:24 2005 +0200
@@ -255,7 +255,7 @@
 
   (* joining of registrations: prefix and attributs of left theory,
      thms are equal, no attempt to subsumption testing *)
-  val join = Termtab.join (fn (reg, _) => SOME reg);
+  fun join x = Termtab.join (fn (reg, _) => SOME reg) x;
 
   fun dest regs = map (apfst untermify) (Termtab.dest regs);