diff --git a/Lambda.ag b/Lambda.ag
--- a/Lambda.ag
+++ b/Lambda.ag
@@ -4,6 +4,7 @@
                  showNameless, showTR, showTRNameless, combinations, synthesise,
                  scoped_Syn_R, deBruijn_Syn_R, dfa_Syn_R, readback_Syn_R, proof_Syn_R, unscoped_Syn_R}
 {
+import Data.Maybe (mapMaybe)
 import Data.Set (Set)
 import qualified Data.Set as Set
 import Data.Map (Map)
@@ -23,17 +24,13 @@
 {type V = String} -- variables
 
 
--- <chunk: data>
--- <chunk: simple-data>
 data Λ -- multi-purpose type for λ-terms
 	| V  var ∷ V                   -- variable
 	| A  fun ∷ Λ        arg   ∷ Λ  -- application
 	| Λ  var ∷ V        body  ∷ Λ  -- lambda
 	| L  binds ∷ Binds  body  ∷ Λ  -- let binding
--- </chunk: simple-data>
 	| S  var ∷ V        body  ∷ Λ  -- adbmal / scope delimiter
 	| I  var ∷ V        body  ∷ Λ  -- indirection node
--- </chunk: data>
 
 type Binds = [Bind]
 type Bind  = (V,Λ)
@@ -320,7 +317,7 @@
 	show lpl = case lpl of
 		MaxPrefix → "maximal prefix lengths"
 		MinPrefix → "minimal prefix lengths"
-		MaxEagPre → "maximal prefix lengths while maintaining eager scope-closure"
+		MaxEagPre → "maximal prefix lengths but eager scope"
 }
 
 -- {type Prefix = [V]}
@@ -587,8 +584,9 @@
 		else infer "S" [mkProof isLetVar name assumptions (tail prefix) term (numS - 1)] conclusion
 
 mkPrefix ∷ Prefix → Box
-mkPrefix prefix = text $ "(" ⧺ unwords (map showVar $ reverse prefix) ⧺ ")"
-	where showVar (v,fs) = v ⧺ if Set.null fs then "" else "[" ⧺ unwords (Set.toList fs) ⧺ "]"
+mkPrefix prefix = text $ "(" ⧺ unwords (mapMaybe showVar $ reverse prefix) ⧺ ")"
+	where showVar (v,fs) = if v == "*" ∧ Set.null fs then Nothing
+		else Just $ v ⧺ if Set.null fs then "" else "{" ⧺ unwords (Set.toList fs) ⧺ "}"
 }
 
 attr R Λ Bind
diff --git a/MaxSharing.hs b/MaxSharing.hs
--- a/MaxSharing.hs
+++ b/MaxSharing.hs
@@ -63,8 +63,8 @@
 	let λTermSyn = syn λTerm
 	putStrLn $ "translation used: " ⧺ show (letPrefixLengths params) ⧺ "\n"
 	let scoped = scoped_Syn_R λTermSyn
-	putStrLn ("scoped (with adbmals):") >> print scoped
-	putStrLn ("scoped (with scope delimiters and nameless abstractions):") >> putStrLn (showNameless scoped)
+	putStrLn ("scoped (adbmals):") >> print scoped
+	putStrLn ("scoped (nameless):") >> putStrLn (showNameless scoped)
 	putStrLn "derivation:" >> putStrLn (render $ proof_Syn_R λTermSyn)
 	let dfa = dfa_Syn_R $ syn scoped
 	putStr "DFA: " >> dot (f ⧺ ".dfa") dfa >> putStrLn ""
diff --git a/examples/not-ll-expr-1.l b/examples/not-ll-expr-1.l
new file mode 100644
--- /dev/null
+++ b/examples/not-ll-expr-1.l
@@ -0,0 +1,1 @@
+let f = \x.\y. f y x in f a b c d e g
diff --git a/examples/running_eff.l b/examples/running_eff.l
new file mode 100644
--- /dev/null
+++ b/examples/running_eff.l
@@ -0,0 +1,1 @@
+\x. \f. let  r = f r x  in  r
diff --git a/examples/running_ineff.l b/examples/running_ineff.l
new file mode 100644
--- /dev/null
+++ b/examples/running_ineff.l
@@ -0,0 +1,1 @@
+\x. \f. let  r = f (f r x) x  in  r
diff --git a/examples/sum.l b/examples/sum.l
new file mode 100644
--- /dev/null
+++ b/examples/sum.l
@@ -0,0 +1,5 @@
+let
+	sum list = case list of
+		Nil -> 0
+		Cons z zs -> (\x.λy -> + x y) z (sum zs)
+in sum (Cons 1 (Cons 2 Nil))
diff --git a/maxsharing.cabal b/maxsharing.cabal
--- a/maxsharing.cabal
+++ b/maxsharing.cabal
@@ -1,5 +1,5 @@
 Name:           maxsharing
-Version:        1.0.2
+Version:        1.0.3
 Copyright:      (c) 2013, Jan Rochel
 Author:         Jan Rochel
 Maintainer:     jan@rochel.info
@@ -10,13 +10,13 @@
 Build-type:     Custom
 Synopsis:       Maximal sharing of terms in the lambda calculus with letrec
 Description:    Parses a lambda-letrec term; transforms it into a first-order
-                term graph representation; minimises the graph; reads back a
-                lambda-letrec term which has the same unfolding as the original
-                term, but exhibits maximal sharing.
+                term graph representation; minimises the graph by bisimulation
+                collapse; reads back a lambda-letrec term which has the same
+                unfolding as the original term but is more (maximally) compact.
                 If executable "dot" from graphviz is available, the graphs are
-                displayed (tested for Linux).
-                The approach is described in a technical report:
-                http://arxiv.org/abs/1401.1460
+                displayed (tested for Linux). The approach is described in an
+                ICFP-paper (http://dx.doi.org/10.1145/2628136.2628148) and an
+                extended version thereof (http://arxiv.org/abs/1401.1460).
 Category:       Graphs, Compiler
 Cabal-Version:  >= 1.6
 Extra-Source-Files: uuagc_options
@@ -32,10 +32,10 @@
     containers-unicode-symbols < 0.4,
     mtl < 2.3,
     uuagc-cabal < 1.1,
-    uuagc >= 0.9.50.2,
-    HaLeX >= 1.2.1,
+    uuagc >= 0.9.50.2 && < 0.10,
+    HaLeX >= 1.2.1 && < 1.3,
     boxes < 0.2,
-    process < 1.2
+    process < 1.5
   Extensions: UnicodeSyntax
   Other-Modules:  Lambda Parser Spanning
   Main-Is: MaxSharing.hs