made smlnj happy;
authorwenzelm
Mon, 12 Jun 2006 11:59:25 +0200
changeset 19853 cb73c3c367db
parent 19852 b06db8e4476b
child 19854 9c1732a66b0b
made smlnj happy;
src/Provers/IsaPlanner/zipper.ML
--- a/src/Provers/IsaPlanner/zipper.ML	Mon Jun 12 09:14:41 2006 +0200
+++ b/src/Provers/IsaPlanner/zipper.ML	Mon Jun 12 11:59:25 2006 +0200
@@ -229,8 +229,8 @@
   fun mktop t = (t, C.empty) : T
 
   val mk = I;
-  val set_trm = apfst o K;
-  val set_ctxt = apsnd o K;
+  fun set_trm x = apfst (K x);
+  fun set_ctxt x = apsnd (K x);
 
   fun goto_top (z as (t,c)) = 
       if C.is_empty c then z else (C.apply c t, C.empty);
@@ -243,11 +243,11 @@
   val ctxt = snd;
   val trm = fst;
 
-  val nty_ctxt = C.nty_ctxt o ctxt;
-  val ty_ctxt = C.ty_ctxt o ctxt;
+  fun nty_ctxt x = C.nty_ctxt (ctxt x);
+  fun ty_ctxt x = C.ty_ctxt (ctxt x);
 
-  val depth_of_ctxt = C.depth o ctxt;
-  val map_on_ctxt = apsnd o C.map;
+  fun depth_of_ctxt x = C.depth (ctxt x);
+  fun map_on_ctxt x = apsnd (C.map x);
   fun fold_on_ctxt f = C.fold f o ctxt;
 
   fun omove_up (t,(d::c)) = SOME (D.apply d t, c)