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