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