diff -r c2ce4797321a -r 7a24d827cba9 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Mon Jul 11 12:23:44 2011 +0100
+++ b/Nominal/Nominal2.thy	Mon Jul 11 14:02:13 2011 +0200
@@ -215,27 +215,6 @@
 end
 *}
 
-ML {*
-infix 1 ||>>> |>>>
-
-fun (x |>>> f) = 
-  let 
-    val (x', y') = f x 
-  in
-    ([x'], y')
-  end
-
-fun (([], y) ||>>> f) = ([], y)  
-  | ((xs, y) ||>>> f) =
-       let
-         val (x', y') = f y
-       in
-         (xs @ [x'], y')
-       end;
-(op ||>>)
-*}
-
-
 
 ML {*
 fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy =