# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1293052412 0
# Node ID 02b24877be3efb30e05394962d31e3ffe7be9da5
# Parent  81921f8ad24553fb6344c23a35303009bd758bfc
added fold_right which produces the correct term for left-infix operators

diff -r 81921f8ad245 -r 02b24877be3e Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Wed Dec 22 12:47:09 2010 +0000
+++ b/Nominal/Nominal2.thy	Wed Dec 22 21:13:32 2010 +0000
@@ -44,11 +44,26 @@
   | mk_union_env tys (t1, @{term "set ([]::atom list)"}) = t1
   | mk_union_env tys (@{term "set ([]::atom list)"}, t2) = t2
   | mk_union_env tys (t1, t2) = mk_binop_env tys @{const_name "sup"} (t1, t2)  
+*}
 
-fun fold_union_env tys trms = fold_rev (curry (mk_union_env tys)) trms @{term "{}::atom set"}
+ML {*
+fun fold_left f [] z = z
+  | fold_left f [x] z = x
+  | fold_left f (x :: y :: xs) z = fold_left f (f (x, y) :: xs) z
+*}
 
+ML {*
+fun fold_union_env tys trms = fold_left (mk_union_env tys) trms @{term "{}::atom set"} 
 *}
 
+ML {*
+fold_union_env [] [@{term "t1::atom set"}, @{term "t2::atom set"}, @{term "t3::atom set"}]
+|> Syntax.string_of_term @{context}
+|> writeln
+*}
+
+
+
 
 ML {*
 fun process_ecase lthy c (params, prems, concl) bclauses =