# HG changeset patch
# User paulson
# Date 1115196293 -7200
# Node ID ed29db71c631b7df9da60f9df393fae3cdc54139
# Parent  01d5d0c1c078f22cc3dc6c7e75910b9fdd68e11d
eta-expansion

diff -r 01d5d0c1c078 -r ed29db71c631 src/Pure/IsaPlanner/isand.ML
--- a/src/Pure/IsaPlanner/isand.ML	Wed May 04 10:42:43 2005 +0200
+++ b/src/Pure/IsaPlanner/isand.ML	Wed May 04 10:44:53 2005 +0200
@@ -170,8 +170,9 @@
           | trec (v as TVar _) = v;
     in trec ty end;
 
-(* implicit typ's and term *)
-val allify_term_typs = Term.map_term_types o allify_typ;
+(* implicit types and term *)
+fun allify_term_typs ty = Term.map_term_types (allify_typ ty);
+
 (* allified version of term, given frees and types to allify over *)
 fun assume_allified sgn (vs,tyvs) t = 
     let