author | paulson |
Tue, 26 Apr 2005 17:44:24 +0200 | |
changeset 15842 | 30a4267c6301 |
parent 15841 | 29bda008409e |
child 15843 | d5bd4a18ce70 |
--- 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);