# HG changeset patch
# User paulson
# Date 849021966 -3600
# Node ID 64acb485eccef3cdd39acde0a5938f58a9e78913
# Parent  f381c1a98209dde7d914feb9c32ee35094e76305
Eta-expansion of a function definition, for value polymorphism

diff -r f381c1a98209 -r 64acb485ecce src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Tue Nov 26 16:18:42 1996 +0100
+++ b/src/Pure/Syntax/ast.ML	Tue Nov 26 16:26:06 1996 +0100
@@ -173,7 +173,7 @@
 struct
   val empty = [];
   val add = op ::;
-  val get = the o assoc;
+  fun get (alist,x) = the (assoc (alist,x));
 end;
 
 
diff -r f381c1a98209 -r 64acb485ecce src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Tue Nov 26 16:18:42 1996 +0100
+++ b/src/Pure/Syntax/parser.ML	Tue Nov 26 16:26:06 1996 +0100
@@ -859,8 +859,8 @@
        end));
 
 
-val get_trees = mapfilter (fn (_, _, [pt], _, _, _) => Some pt | _ => None);
-
+fun get_trees l = mapfilter (fn (_, _, [pt], _, _, _) => Some pt | _ => None) 
+                            l;
 
 fun earley prods tags chains startsymbol indata =
   let
diff -r f381c1a98209 -r 64acb485ecce src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Tue Nov 26 16:18:42 1996 +0100
+++ b/src/Pure/Syntax/printer.ML	Tue Nov 26 16:26:06 1996 +0100
@@ -131,7 +131,7 @@
 
 type prtabs = (string * ((symb list * int * int) list) Symtab.table) list;
 
-val prmodes_of = filter_out (equal "") o map fst;
+fun prmodes_of l = filter_out (equal "") (map fst l);
 
 (*find tab for mode*)
 fun get_tab prtabs mode =