src/Pure/Isar/locale.ML

           | ut (s $ t) ts = ut s (t::ts)
     in ut t [] end;
 
   (* 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);
 
   (* registrations that subsume t *)
   fun subsumers tsig t regs =