# HG changeset patch
# User haftmann
# Date 1283873793 -7200
# Node ID 202618462644951dffcbb719ab10dde20c4ad90e
# Parent  234e6ef4ff67378463186653b6a05e6b2d19bc51# Parent  985b13c5a61d2fcc7f09397b2e4d151989db1410
merged

diff -r 234e6ef4ff67 -r 202618462644 doc-src/Classes/Thy/document/Classes.tex
--- a/doc-src/Classes/Thy/document/Classes.tex	Tue Sep 07 14:11:05 2010 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex	Tue Sep 07 17:36:33 2010 +0200
@@ -1134,65 +1134,64 @@
 \noindent%
 \hspace*{0pt}module Example where {\char123}\\
 \hspace*{0pt}\\
-\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Example.Nat;\\
+\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
 \hspace*{0pt}\\
-\hspace*{0pt}nat{\char95}aux ::~Integer -> Example.Nat -> Example.Nat;\\
-\hspace*{0pt}nat{\char95}aux i n =\\
-\hspace*{0pt} ~(if i <= 0 then n else Example.nat{\char95}aux (i - 1) (Example.Suc n));\\
+\hspace*{0pt}nat{\char95}aux ::~Integer -> Nat -> Nat;\\
+\hspace*{0pt}nat{\char95}aux i n = (if i <= 0 then n else nat{\char95}aux (i - 1) (Suc n));\\
 \hspace*{0pt}\\
-\hspace*{0pt}nat ::~Integer -> Example.Nat;\\
-\hspace*{0pt}nat i = Example.nat{\char95}aux i Example.Zero{\char95}nat;\\
+\hspace*{0pt}nat ::~Integer -> Nat;\\
+\hspace*{0pt}nat i = nat{\char95}aux i Zero{\char95}nat;\\
 \hspace*{0pt}\\
 \hspace*{0pt}class Semigroup a where {\char123}\\
 \hspace*{0pt} ~mult ::~a -> a -> a;\\
 \hspace*{0pt}{\char125};\\
 \hspace*{0pt}\\
-\hspace*{0pt}class (Example.Semigroup a) => Monoidl a where {\char123}\\
+\hspace*{0pt}class (Semigroup a) => Monoidl a where {\char123}\\
 \hspace*{0pt} ~neutral ::~a;\\
 \hspace*{0pt}{\char125};\\
 \hspace*{0pt}\\
-\hspace*{0pt}class (Example.Monoidl a) => Monoid a where {\char123}\\
+\hspace*{0pt}class (Monoidl a) => Monoid a where {\char123}\\
+\hspace*{0pt}{\char125};\\
+\hspace*{0pt}\\
+\hspace*{0pt}class (Monoid a) => Group a where {\char123}\\
+\hspace*{0pt} ~inverse ::~a -> a;\\
 \hspace*{0pt}{\char125};\\
 \hspace*{0pt}\\
-\hspace*{0pt}class (Example.Monoid a) => Group a where {\char123}\\
-\hspace*{0pt} ~inverse ::~a -> a;\\
-\hspace*{0pt}{\char125};\\
+\hspace*{0pt}pow{\char95}nat ::~forall a.~(Monoid a) => Nat -> a -> a;\\
+\hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\
+\hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\
+\hspace*{0pt}\\
+\hspace*{0pt}pow{\char95}int ::~forall a.~(Group a) => Integer -> a -> a;\\
+\hspace*{0pt}pow{\char95}int k x =\\
+\hspace*{0pt} ~(if 0 <= k then pow{\char95}nat (nat k) x\\
+\hspace*{0pt} ~~~else inverse (pow{\char95}nat (nat (negate k)) x));\\
 \hspace*{0pt}\\
 \hspace*{0pt}mult{\char95}int ::~Integer -> Integer -> Integer;\\
 \hspace*{0pt}mult{\char95}int i j = i + j;\\
 \hspace*{0pt}\\
+\hspace*{0pt}instance Semigroup Integer where {\char123}\\
+\hspace*{0pt} ~mult = mult{\char95}int;\\
+\hspace*{0pt}{\char125};\\
+\hspace*{0pt}\\
 \hspace*{0pt}neutral{\char95}int ::~Integer;\\
 \hspace*{0pt}neutral{\char95}int = 0;\\
 \hspace*{0pt}\\
+\hspace*{0pt}instance Monoidl Integer where {\char123}\\
+\hspace*{0pt} ~neutral = neutral{\char95}int;\\
+\hspace*{0pt}{\char125};\\
+\hspace*{0pt}\\
+\hspace*{0pt}instance Monoid Integer where {\char123}\\
+\hspace*{0pt}{\char125};\\
+\hspace*{0pt}\\
 \hspace*{0pt}inverse{\char95}int ::~Integer -> Integer;\\
 \hspace*{0pt}inverse{\char95}int i = negate i;\\
 \hspace*{0pt}\\
-\hspace*{0pt}instance Example.Semigroup Integer where {\char123}\\
-\hspace*{0pt} ~mult = Example.mult{\char95}int;\\
-\hspace*{0pt}{\char125};\\
-\hspace*{0pt}\\
-\hspace*{0pt}instance Example.Monoidl Integer where {\char123}\\
-\hspace*{0pt} ~neutral = Example.neutral{\char95}int;\\
-\hspace*{0pt}{\char125};\\
-\hspace*{0pt}\\
-\hspace*{0pt}instance Example.Monoid Integer where {\char123}\\
+\hspace*{0pt}instance Group Integer where {\char123}\\
+\hspace*{0pt} ~inverse = inverse{\char95}int;\\
 \hspace*{0pt}{\char125};\\
 \hspace*{0pt}\\
-\hspace*{0pt}instance Example.Group Integer where {\char123}\\
-\hspace*{0pt} ~inverse = Example.inverse{\char95}int;\\
-\hspace*{0pt}{\char125};\\
-\hspace*{0pt}\\
-\hspace*{0pt}pow{\char95}nat ::~forall a.~(Example.Monoid a) => Example.Nat -> a -> a;\\
-\hspace*{0pt}pow{\char95}nat Example.Zero{\char95}nat x = Example.neutral;\\
-\hspace*{0pt}pow{\char95}nat (Example.Suc n) x = Example.mult x (Example.pow{\char95}nat n x);\\
-\hspace*{0pt}\\
-\hspace*{0pt}pow{\char95}int ::~forall a.~(Example.Group a) => Integer -> a -> a;\\
-\hspace*{0pt}pow{\char95}int k x =\\
-\hspace*{0pt} ~(if 0 <= k then Example.pow{\char95}nat (Example.nat k) x\\
-\hspace*{0pt} ~~~else Example.inverse (Example.pow{\char95}nat (Example.nat (negate k)) x));\\
-\hspace*{0pt}\\
 \hspace*{0pt}example ::~Integer;\\
-\hspace*{0pt}example = Example.pow{\char95}int 10 (-2);\\
+\hspace*{0pt}example = pow{\char95}int 10 (-2);\\
 \hspace*{0pt}\\
 \hspace*{0pt}{\char125}%
 \end{isamarkuptext}%
diff -r 234e6ef4ff67 -r 202618462644 doc-src/Codegen/Thy/document/Foundations.tex
--- a/doc-src/Codegen/Thy/document/Foundations.tex	Tue Sep 07 14:11:05 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Foundations.tex	Tue Sep 07 17:36:33 2010 +0200
@@ -247,11 +247,11 @@
 \begin{isamarkuptext}%
 \isatypewriter%
 \noindent%
-\hspace*{0pt}dequeue ::~forall a.~Example.Queue a -> (Maybe a,~Example.Queue a);\\
-\hspace*{0pt}dequeue (Example.AQueue xs (y :~ys)) = (Just y,~Example.AQueue xs ys);\\
-\hspace*{0pt}dequeue (Example.AQueue xs []) =\\
-\hspace*{0pt} ~(if null xs then (Nothing,~Example.AQueue [] [])\\
-\hspace*{0pt} ~~~else Example.dequeue (Example.AQueue [] (reverse xs)));%
+\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
+\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
+\hspace*{0pt}dequeue (AQueue xs []) =\\
+\hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\
+\hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -444,12 +444,12 @@
 \begin{isamarkuptext}%
 \isatypewriter%
 \noindent%
-\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Example.Queue a -> (a,~Example.Queue a);\\
-\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs []) =\\
+\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
+\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
 \hspace*{0pt} ~let {\char123}\\
 \hspace*{0pt} ~~~(y :~ys) = reverse xs;\\
-\hspace*{0pt} ~{\char125}~in (y,~Example.AQueue [] ys);\\
-\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs (y :~ys)) = (y,~Example.AQueue xs ys);%
+\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
+\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -538,11 +538,11 @@
 \hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\
 \hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
 \hspace*{0pt}\\
-\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Example.Queue a -> (a,~Example.Queue a);\\
-\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs (y :~ys)) = (y,~Example.AQueue xs ys);\\
-\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs []) =\\
-\hspace*{0pt} ~(if null xs then Example.empty{\char95}queue\\
-\hspace*{0pt} ~~~else Example.strict{\char95}dequeue (Example.AQueue [] (reverse xs)));%
+\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
+\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
+\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
+\hspace*{0pt} ~(if null xs then empty{\char95}queue\\
+\hspace*{0pt} ~~~else strict{\char95}dequeue (AQueue [] (reverse xs)));%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r 234e6ef4ff67 -r 202618462644 doc-src/Codegen/Thy/document/Further.tex
--- a/doc-src/Codegen/Thy/document/Further.tex	Tue Sep 07 14:11:05 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex	Tue Sep 07 17:36:33 2010 +0200
@@ -216,13 +216,13 @@
 \begin{isamarkuptext}%
 \isatypewriter%
 \noindent%
-\hspace*{0pt}funpow ::~forall a.~Example.Nat -> (a -> a) -> a -> a;\\
-\hspace*{0pt}funpow Example.Zero{\char95}nat f = id;\\
-\hspace*{0pt}funpow (Example.Suc n) f = f .~Example.funpow n f;\\
+\hspace*{0pt}funpow ::~forall a.~Nat -> (a -> a) -> a -> a;\\
+\hspace*{0pt}funpow Zero{\char95}nat f = id;\\
+\hspace*{0pt}funpow (Suc n) f = f .~funpow n f;\\
 \hspace*{0pt}\\
-\hspace*{0pt}funpows ::~forall a.~[Example.Nat] -> (a -> a) -> a -> a;\\
+\hspace*{0pt}funpows ::~forall a.~[Nat] -> (a -> a) -> a -> a;\\
 \hspace*{0pt}funpows [] = id;\\
-\hspace*{0pt}funpows (x :~xs) = Example.funpow x .~Example.funpows xs;%
+\hspace*{0pt}funpows (x :~xs) = funpow x .~funpows xs;%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r 234e6ef4ff67 -r 202618462644 doc-src/Codegen/Thy/document/Introduction.tex
--- a/doc-src/Codegen/Thy/document/Introduction.tex	Tue Sep 07 14:11:05 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex	Tue Sep 07 17:36:33 2010 +0200
@@ -231,19 +231,19 @@
 \hspace*{0pt}\\
 \hspace*{0pt}data Queue a = AQueue [a] [a];\\
 \hspace*{0pt}\\
-\hspace*{0pt}empty ::~forall a.~Example.Queue a;\\
-\hspace*{0pt}empty = Example.AQueue [] [];\\
+\hspace*{0pt}empty ::~forall a.~Queue a;\\
+\hspace*{0pt}empty = AQueue [] [];\\
 \hspace*{0pt}\\
-\hspace*{0pt}dequeue ::~forall a.~Example.Queue a -> (Maybe a,~Example.Queue a);\\
-\hspace*{0pt}dequeue (Example.AQueue [] []) = (Nothing,~Example.AQueue [] []);\\
-\hspace*{0pt}dequeue (Example.AQueue xs (y :~ys)) = (Just y,~Example.AQueue xs ys);\\
-\hspace*{0pt}dequeue (Example.AQueue (v :~va) []) =\\
+\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
+\hspace*{0pt}dequeue (AQueue [] []) = (Nothing,~AQueue [] []);\\
+\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
+\hspace*{0pt}dequeue (AQueue (v :~va) []) =\\
 \hspace*{0pt} ~let {\char123}\\
 \hspace*{0pt} ~~~(y :~ys) = reverse (v :~va);\\
-\hspace*{0pt} ~{\char125}~in (Just y,~Example.AQueue [] ys);\\
+\hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys);\\
 \hspace*{0pt}\\
-\hspace*{0pt}enqueue ::~forall a.~a -> Example.Queue a -> Example.Queue a;\\
-\hspace*{0pt}enqueue x (Example.AQueue xs ys) = Example.AQueue (x :~xs) ys;\\
+\hspace*{0pt}enqueue ::~forall a.~a -> Queue a -> Queue a;\\
+\hspace*{0pt}enqueue x (AQueue xs ys) = AQueue (x :~xs) ys;\\
 \hspace*{0pt}\\
 \hspace*{0pt}{\char125}%
 \end{isamarkuptext}%
@@ -397,41 +397,41 @@
 \noindent%
 \hspace*{0pt}module Example where {\char123}\\
 \hspace*{0pt}\\
-\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Example.Nat;\\
+\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
 \hspace*{0pt}\\
-\hspace*{0pt}plus{\char95}nat ::~Example.Nat -> Example.Nat -> Example.Nat;\\
-\hspace*{0pt}plus{\char95}nat (Example.Suc m) n = Example.plus{\char95}nat m (Example.Suc n);\\
-\hspace*{0pt}plus{\char95}nat Example.Zero{\char95}nat n = n;\\
+\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\
+\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\
+\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\
 \hspace*{0pt}\\
 \hspace*{0pt}class Semigroup a where {\char123}\\
 \hspace*{0pt} ~mult ::~a -> a -> a;\\
 \hspace*{0pt}{\char125};\\
 \hspace*{0pt}\\
-\hspace*{0pt}class (Example.Semigroup a) => Monoid a where {\char123}\\
+\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\
 \hspace*{0pt} ~neutral ::~a;\\
 \hspace*{0pt}{\char125};\\
 \hspace*{0pt}\\
-\hspace*{0pt}pow ::~forall a.~(Example.Monoid a) => Example.Nat -> a -> a;\\
-\hspace*{0pt}pow Example.Zero{\char95}nat a = Example.neutral;\\
-\hspace*{0pt}pow (Example.Suc n) a = Example.mult a (Example.pow n a);\\
+\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\
+\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\
+\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\
 \hspace*{0pt}\\
-\hspace*{0pt}mult{\char95}nat ::~Example.Nat -> Example.Nat -> Example.Nat;\\
-\hspace*{0pt}mult{\char95}nat Example.Zero{\char95}nat n = Example.Zero{\char95}nat;\\
-\hspace*{0pt}mult{\char95}nat (Example.Suc m) n = Example.plus{\char95}nat n (Example.mult{\char95}nat m n);\\
+\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\
+\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\
+\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
 \hspace*{0pt}\\
-\hspace*{0pt}neutral{\char95}nat ::~Example.Nat;\\
-\hspace*{0pt}neutral{\char95}nat = Example.Suc Example.Zero{\char95}nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}instance Example.Semigroup Example.Nat where {\char123}\\
-\hspace*{0pt} ~mult = Example.mult{\char95}nat;\\
+\hspace*{0pt}instance Semigroup Nat where {\char123}\\
+\hspace*{0pt} ~mult = mult{\char95}nat;\\
 \hspace*{0pt}{\char125};\\
 \hspace*{0pt}\\
-\hspace*{0pt}instance Example.Monoid Example.Nat where {\char123}\\
-\hspace*{0pt} ~neutral = Example.neutral{\char95}nat;\\
+\hspace*{0pt}neutral{\char95}nat ::~Nat;\\
+\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\
+\hspace*{0pt}\\
+\hspace*{0pt}instance Monoid Nat where {\char123}\\
+\hspace*{0pt} ~neutral = neutral{\char95}nat;\\
 \hspace*{0pt}{\char125};\\
 \hspace*{0pt}\\
-\hspace*{0pt}bexp ::~Example.Nat -> Example.Nat;\\
-\hspace*{0pt}bexp n = Example.pow n (Example.Suc (Example.Suc Example.Zero{\char95}nat));\\
+\hspace*{0pt}bexp ::~Nat -> Nat;\\
+\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\
 \hspace*{0pt}\\
 \hspace*{0pt}{\char125}%
 \end{isamarkuptext}%
diff -r 234e6ef4ff67 -r 202618462644 doc-src/Codegen/Thy/document/Refinement.tex
--- a/doc-src/Codegen/Thy/document/Refinement.tex	Tue Sep 07 14:11:05 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Refinement.tex	Tue Sep 07 17:36:33 2010 +0200
@@ -74,11 +74,10 @@
 \begin{isamarkuptext}%
 \isatypewriter%
 \noindent%
-\hspace*{0pt}fib ::~Example.Nat -> Example.Nat;\\
-\hspace*{0pt}fib Example.Zero{\char95}nat = Example.Zero{\char95}nat;\\
-\hspace*{0pt}fib (Example.Suc Example.Zero{\char95}nat) = Example.Suc Example.Zero{\char95}nat;\\
-\hspace*{0pt}fib (Example.Suc (Example.Suc n)) =\\
-\hspace*{0pt} ~Example.plus{\char95}nat (Example.fib n) (Example.fib (Example.Suc n));%
+\hspace*{0pt}fib ::~Nat -> Nat;\\
+\hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;\\
+\hspace*{0pt}fib (Suc Zero{\char95}nat) = Suc Zero{\char95}nat;\\
+\hspace*{0pt}fib (Suc (Suc n)) = plus{\char95}nat (fib n) (fib (Suc n));%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -173,17 +172,15 @@
 \begin{isamarkuptext}%
 \isatypewriter%
 \noindent%
-\hspace*{0pt}fib{\char95}step ::~Example.Nat -> (Example.Nat,~Example.Nat);\\
-\hspace*{0pt}fib{\char95}step (Example.Suc n) =\\
-\hspace*{0pt} ~let {\char123}\\
-\hspace*{0pt} ~~~(m,~q) = Example.fib{\char95}step n;\\
-\hspace*{0pt} ~{\char125}~in (Example.plus{\char95}nat m q,~m);\\
-\hspace*{0pt}fib{\char95}step Example.Zero{\char95}nat =\\
-\hspace*{0pt} ~(Example.Suc Example.Zero{\char95}nat,~Example.Zero{\char95}nat);\\
+\hspace*{0pt}fib{\char95}step ::~Nat -> (Nat,~Nat);\\
+\hspace*{0pt}fib{\char95}step (Suc n) = let {\char123}\\
+\hspace*{0pt} ~~~~~~~~~~~~~~~~~~~~(m,~q) = fib{\char95}step n;\\
+\hspace*{0pt} ~~~~~~~~~~~~~~~~~~{\char125}~in (plus{\char95}nat m q,~m);\\
+\hspace*{0pt}fib{\char95}step Zero{\char95}nat = (Suc Zero{\char95}nat,~Zero{\char95}nat);\\
 \hspace*{0pt}\\
-\hspace*{0pt}fib ::~Example.Nat -> Example.Nat;\\
-\hspace*{0pt}fib (Example.Suc n) = fst (Example.fib{\char95}step n);\\
-\hspace*{0pt}fib Example.Zero{\char95}nat = Example.Zero{\char95}nat;%
+\hspace*{0pt}fib ::~Nat -> Nat;\\
+\hspace*{0pt}fib (Suc n) = fst (fib{\char95}step n);\\
+\hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -593,30 +590,28 @@
 \hspace*{0pt}\\
 \hspace*{0pt}newtype Dlist a = Dlist [a];\\
 \hspace*{0pt}\\
-\hspace*{0pt}empty ::~forall a.~Example.Dlist a;\\
-\hspace*{0pt}empty = Example.Dlist [];\\
+\hspace*{0pt}empty ::~forall a.~Dlist a;\\
+\hspace*{0pt}empty = Dlist [];\\
 \hspace*{0pt}\\
 \hspace*{0pt}member ::~forall a.~(Eq a) => [a] -> a -> Bool;\\
 \hspace*{0pt}member [] y = False;\\
-\hspace*{0pt}member (x :~xs) y = x == y || Example.member xs y;\\
+\hspace*{0pt}member (x :~xs) y = x == y || member xs y;\\
 \hspace*{0pt}\\
-\hspace*{0pt}inserta ::~forall a.~(Eq a) => a -> [a] -> [a];\\
-\hspace*{0pt}inserta x xs = (if Example.member xs x then xs else x :~xs);\\
+\hspace*{0pt}insert ::~forall a.~(Eq a) => a -> [a] -> [a];\\
+\hspace*{0pt}insert x xs = (if member xs x then xs else x :~xs);\\
 \hspace*{0pt}\\
-\hspace*{0pt}list{\char95}of{\char95}dlist ::~forall a.~Example.Dlist a -> [a];\\
-\hspace*{0pt}list{\char95}of{\char95}dlist (Example.Dlist x) = x;\\
+\hspace*{0pt}list{\char95}of{\char95}dlist ::~forall a.~Dlist a -> [a];\\
+\hspace*{0pt}list{\char95}of{\char95}dlist (Dlist x) = x;\\
 \hspace*{0pt}\\
-\hspace*{0pt}insert ::~forall a.~(Eq a) => a -> Example.Dlist a -> Example.Dlist a;\\
-\hspace*{0pt}insert x dxs =\\
-\hspace*{0pt} ~Example.Dlist (Example.inserta x (Example.list{\char95}of{\char95}dlist dxs));\\
+\hspace*{0pt}inserta ::~forall a.~(Eq a) => a -> Dlist a -> Dlist a;\\
+\hspace*{0pt}inserta x dxs = Dlist (insert x (list{\char95}of{\char95}dlist dxs));\\
 \hspace*{0pt}\\
 \hspace*{0pt}remove1 ::~forall a.~(Eq a) => a -> [a] -> [a];\\
 \hspace*{0pt}remove1 x [] = [];\\
-\hspace*{0pt}remove1 x (y :~xs) = (if x == y then xs else y :~Example.remove1 x xs);\\
+\hspace*{0pt}remove1 x (y :~xs) = (if x == y then xs else y :~remove1 x xs);\\
 \hspace*{0pt}\\
-\hspace*{0pt}remove ::~forall a.~(Eq a) => a -> Example.Dlist a -> Example.Dlist a;\\
-\hspace*{0pt}remove x dxs =\\
-\hspace*{0pt} ~Example.Dlist (Example.remove1 x (Example.list{\char95}of{\char95}dlist dxs));\\
+\hspace*{0pt}remove ::~forall a.~(Eq a) => a -> Dlist a -> Dlist a;\\
+\hspace*{0pt}remove x dxs = Dlist (remove1 x (list{\char95}of{\char95}dlist dxs));\\
 \hspace*{0pt}\\
 \hspace*{0pt}{\char125}%
 \end{isamarkuptext}%
diff -r 234e6ef4ff67 -r 202618462644 doc-src/Codegen/Thy/examples/Example.hs
--- a/doc-src/Codegen/Thy/examples/Example.hs	Tue Sep 07 14:11:05 2010 +0200
+++ b/doc-src/Codegen/Thy/examples/Example.hs	Tue Sep 07 17:36:33 2010 +0200
@@ -4,18 +4,18 @@
 
 data Queue a = AQueue [a] [a];
 
-empty :: forall a. Example.Queue a;
-empty = Example.AQueue [] [];
+empty :: forall a. Queue a;
+empty = AQueue [] [];
 
-dequeue :: forall a. Example.Queue a -> (Maybe a, Example.Queue a);
-dequeue (Example.AQueue [] []) = (Nothing, Example.AQueue [] []);
-dequeue (Example.AQueue xs (y : ys)) = (Just y, Example.AQueue xs ys);
-dequeue (Example.AQueue (v : va) []) =
+dequeue :: forall a. Queue a -> (Maybe a, Queue a);
+dequeue (AQueue [] []) = (Nothing, AQueue [] []);
+dequeue (AQueue xs (y : ys)) = (Just y, AQueue xs ys);
+dequeue (AQueue (v : va) []) =
   let {
     (y : ys) = reverse (v : va);
-  } in (Just y, Example.AQueue [] ys);
+  } in (Just y, AQueue [] ys);
 
-enqueue :: forall a. a -> Example.Queue a -> Example.Queue a;
-enqueue x (Example.AQueue xs ys) = Example.AQueue (x : xs) ys;
+enqueue :: forall a. a -> Queue a -> Queue a;
+enqueue x (AQueue xs ys) = AQueue (x : xs) ys;
 
 }
diff -r 234e6ef4ff67 -r 202618462644 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Tue Sep 07 14:11:05 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Tue Sep 07 17:36:33 2010 +0200
@@ -27,7 +27,6 @@
 fun print_haskell_stmt labelled_name class_syntax tyco_syntax const_syntax
     reserved deresolve contr_classparam_typs deriving_show =
   let
-    val deresolve_base = Long_Name.base_name o deresolve;
     fun class_name class = case class_syntax class
      of NONE => deresolve class
       | SOME class => class;
@@ -121,7 +120,7 @@
             val tyvars = intro_vars (map fst vs) reserved;
             fun print_err n =
               semicolon (
-                (str o deresolve_base) name
+                (str o deresolve) name
                 :: map str (replicate n "_")
                 @ str "="
                 :: str "error"
@@ -138,7 +137,7 @@
                       (insert (op =)) ts []);
               in
                 semicolon (
-                  (str o deresolve_base) name
+                  (str o deresolve) name
                   :: map (print_term tyvars some_thm vars BR) ts
                   @ str "="
                   @@ print_term tyvars some_thm vars NOBR t
@@ -147,7 +146,7 @@
           in
             Pretty.chunks (
               semicolon [
-                (str o suffix " ::" o deresolve_base) name,
+                (str o suffix " ::" o deresolve) name,
                 print_typscheme tyvars (vs, ty)
               ]
               :: (case filter (snd o snd) raw_eqs
@@ -161,7 +160,7 @@
           in
             semicolon [
               str "data",
-              print_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
+              print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
             ]
           end
       | print_stmt (name, Code_Thingol.Datatype (_, (vs, [((co, _), [ty])]))) =
@@ -170,9 +169,9 @@
           in
             semicolon (
               str "newtype"
-              :: print_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
+              :: print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
               :: str "="
-              :: (str o deresolve_base) co
+              :: (str o deresolve) co
               :: print_typ tyvars BR ty
               :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
             )
@@ -182,13 +181,13 @@
             val tyvars = intro_vars (map fst vs) reserved;
             fun print_co ((co, _), tys) =
               concat (
-                (str o deresolve_base) co
+                (str o deresolve) co
                 :: map (print_typ tyvars BR) tys
               )
           in
             semicolon (
               str "data"
-              :: print_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
+              :: print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
               :: str "="
               :: print_co co
               :: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos
@@ -200,7 +199,7 @@
             val tyvars = intro_vars [v] reserved;
             fun print_classparam (classparam, ty) =
               semicolon [
-                (str o deresolve_base) classparam,
+                (str o deresolve) classparam,
                 str "::",
                 print_typ tyvars NOBR ty
               ]
@@ -209,7 +208,7 @@
               Pretty.block [
                 str "class ",
                 Pretty.block (print_typcontext tyvars [(v, map fst super_classes)]),
-                str (deresolve_base name ^ " " ^ lookup_var tyvars v),
+                str (deresolve name ^ " " ^ lookup_var tyvars v),
                 str " where {"
               ],
               str "};"
@@ -219,17 +218,17 @@
           let
             val tyvars = intro_vars (map fst vs) reserved;
             fun requires_args classparam = case const_syntax classparam
-             of NONE => 0
-              | SOME (Code_Printer.Plain_const_syntax _) => 0
-              | SOME (Code_Printer.Complex_const_syntax (k,_ )) => k;
+             of NONE => NONE
+              | SOME (Code_Printer.Plain_const_syntax _) => SOME 0
+              | SOME (Code_Printer.Complex_const_syntax (k,_ )) => SOME k;
             fun print_classparam_instance ((classparam, const), (thm, _)) =
               case requires_args classparam
-               of 0 => semicolon [
-                      (str o deresolve_base) classparam,
+               of NONE => semicolon [
+                      (str o Long_Name.base_name o deresolve) classparam,
                       str "=",
                       print_app tyvars (SOME thm) reserved NOBR (const, [])
                     ]
-                | k =>
+                | SOME k =>
                     let
                       val (c, (_, tys)) = const;
                       val (vs, rhs) = (apfst o map) fst
@@ -261,82 +260,51 @@
           end;
   in print_stmt end;
 
-fun mk_name_module reserved module_prefix module_alias program =
+fun haskell_program_of_program labelled_name module_alias module_prefix reserved =
   let
-    fun mk_alias name = case module_alias name
-     of SOME name' => name'
-      | NONE => name
-          |> Long_Name.explode
-          |> map (fn name => (the_single o fst) (Name.variants [name] reserved))
-          |> Long_Name.implode;
-    fun mk_prefix name = case module_prefix
-     of SOME module_prefix => Long_Name.append module_prefix name
-      | NONE => name;
-    val tab =
-      Symtab.empty
-      |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
-           o fst o Code_Namespace.dest_name o fst)
-             program
-  in the o Symtab.lookup tab end;
-
-fun haskell_program_of_program labelled_name module_prefix reserved module_alias program =
-  let
-    val reserved = Name.make_context reserved;
-    val mk_name_module = mk_name_module reserved module_prefix module_alias program;
-    fun add_stmt (name, (stmt, deps)) =
+    fun namify_fun upper base (nsp_fun, nsp_typ) =
+      let
+        val (base', nsp_fun') = yield_singleton Name.variants
+          (if upper then first_upper base else base) nsp_fun;
+      in (base', (nsp_fun', nsp_typ)) end;
+    fun namify_typ base (nsp_fun, nsp_typ) =
       let
-        val (module_name, base) = Code_Namespace.dest_name name;
-        val module_name' = mk_name_module module_name;
-        val mk_name_stmt = yield_singleton Name.variants;
-        fun add_fun upper (nsp_fun, nsp_typ) =
-          let
-            val (base', nsp_fun') =
-              mk_name_stmt (if upper then first_upper base else base) nsp_fun
-          in (base', (nsp_fun', nsp_typ)) end;
-        fun add_typ (nsp_fun, nsp_typ) =
-          let
-            val (base', nsp_typ') = mk_name_stmt (first_upper base) nsp_typ
-          in (base', (nsp_fun, nsp_typ')) end;
-        val add_name = case stmt
-         of Code_Thingol.Fun (_, (_, SOME _)) => pair base
-          | Code_Thingol.Fun _ => add_fun false
-          | Code_Thingol.Datatype _ => add_typ
-          | Code_Thingol.Datatypecons _ => add_fun true
-          | Code_Thingol.Class _ => add_typ
-          | Code_Thingol.Classrel _ => pair base
-          | Code_Thingol.Classparam _ => add_fun false
-          | Code_Thingol.Classinst _ => pair base;
-        fun add_stmt' base' = case stmt
-         of Code_Thingol.Fun (_, (_, SOME _)) =>
-              I
-          | Code_Thingol.Datatypecons _ =>
-              cons (name, (Long_Name.append module_name' base', NONE))
-          | Code_Thingol.Classrel _ => I
-          | Code_Thingol.Classparam _ =>
-              cons (name, (Long_Name.append module_name' base', NONE))
-          | _ => cons (name, (Long_Name.append module_name' base', SOME stmt));
-      in
-        Symtab.map_default (module_name', ([], ([], (reserved, reserved))))
-              (apfst (fold (insert (op = : string * string -> bool)) deps))
-        #> `(fn program => add_name ((snd o snd o the o Symtab.lookup program) module_name'))
-        #-> (fn (base', names) =>
-              (Symtab.map_entry module_name' o apsnd) (fn (stmts, _) =>
-              (add_stmt' base' stmts, names)))
-      end;
-    val hs_program = fold add_stmt (AList.make (fn name =>
-      (Graph.get_node program name, Graph.imm_succs program name))
-      (Graph.strong_conn program |> flat)) Symtab.empty;
-    fun deresolver name = (fst o the o AList.lookup (op =) ((fst o snd o the
-      o Symtab.lookup hs_program) ((mk_name_module o fst o Code_Namespace.dest_name) name))) name
-      handle Option => error ("Unknown statement name: " ^ labelled_name name);
-  in (deresolver, hs_program) end;
+        val (base', nsp_typ') = yield_singleton Name.variants
+          (first_upper base) nsp_typ
+      in (base', (nsp_fun, nsp_typ')) end;
+    fun namify_stmt (Code_Thingol.Fun (_, (_, SOME _))) = pair
+      | namify_stmt (Code_Thingol.Fun _) = namify_fun false
+      | namify_stmt (Code_Thingol.Datatype _) = namify_typ
+      | namify_stmt (Code_Thingol.Datatypecons _) = namify_fun true
+      | namify_stmt (Code_Thingol.Class _) = namify_typ
+      | namify_stmt (Code_Thingol.Classrel _) = pair
+      | namify_stmt (Code_Thingol.Classparam _) = namify_fun false
+      | namify_stmt (Code_Thingol.Classinst _) = pair;
+    fun select_stmt (Code_Thingol.Fun (_, (_, SOME _))) = false
+      | select_stmt (Code_Thingol.Fun _) = true
+      | select_stmt (Code_Thingol.Datatype _) = true
+      | select_stmt (Code_Thingol.Datatypecons _) = false
+      | select_stmt (Code_Thingol.Class _) = true
+      | select_stmt (Code_Thingol.Classrel _) = false
+      | select_stmt (Code_Thingol.Classparam _) = false
+      | select_stmt (Code_Thingol.Classinst _) = true;
+  in
+    Code_Namespace.flat_program labelled_name
+      { module_alias = module_alias, module_prefix = module_prefix,
+        reserved = reserved, empty_nsp = (reserved, reserved), namify_stmt = namify_stmt,
+        modify_stmt = fn stmt => if select_stmt stmt then SOME stmt else NONE }
+  end;
 
 fun serialize_haskell module_prefix string_classes { labelled_name, reserved_syms,
     includes, module_alias, class_syntax, tyco_syntax, const_syntax, program } =
   let
+
+    (* build program *)
     val reserved = fold (insert (op =) o fst) includes reserved_syms;
-    val (deresolver, hs_program) = haskell_program_of_program labelled_name
-      module_prefix reserved module_alias program;
+    val { deresolver, flat_program = haskell_program } = haskell_program_of_program
+      labelled_name module_alias module_prefix (Name.make_context reserved) program;
+
+    (* print statements *)
     val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
     fun deriving_show tyco =
       let
@@ -351,62 +319,58 @@
               andalso forall (deriv' tycos) tys
           | deriv' _ (ITyVar _) = true
       in deriv [] tyco end;
-    val reserved = make_vars reserved;
-    fun print_stmt qualified = print_haskell_stmt labelled_name
-      class_syntax tyco_syntax const_syntax reserved
-      (if qualified then deresolver else Long_Name.base_name o deresolver)
-      contr_classparam_typs
+    fun print_stmt deresolve = print_haskell_stmt labelled_name
+      class_syntax tyco_syntax const_syntax (make_vars reserved)
+      deresolve contr_classparam_typs
       (if string_classes then deriving_show else K false);
-    fun print_module name content =
-      (name, Pretty.chunks2 [
-        str ("module " ^ name ^ " where {"),
-        content,
-        str "}"
-      ]);
-    fun serialize_module (module_name', (deps, (stmts, _))) =
+
+    (* print modules *)
+    val import_includes_ps =
+      map (fn (name, _) => str ("import qualified " ^ name ^ ";")) includes;
+    fun print_module_frame module_name ps =
+      (module_name, Pretty.chunks2 (
+        str ("module " ^ module_name ^ " where {")
+        :: ps
+        @| str "}"
+      ));
+    fun print_module module_name (gr, imports) =
       let
-        val stmt_names = map fst stmts;
-        val qualified = true;
-        val imports = subtract (op =) stmt_names deps
-          |> distinct (op =)
-          |> map_filter (try deresolver)
-          |> map Long_Name.qualifier
-          |> distinct (op =);
-        fun print_import_include (name, _) = str ("import qualified " ^ name ^ ";");
-        fun print_import_module name = str ((if qualified
-          then "import qualified "
-          else "import ") ^ name ^ ";");
-        val import_ps = map print_import_include includes @ map print_import_module imports
-        val content = Pretty.chunks2 ((if null import_ps then [] else [Pretty.chunks import_ps])
-            @ map_filter
-              (fn (name, (_, SOME stmt)) => SOME (markup_stmt name (print_stmt qualified (name, stmt)))
-                | (_, (_, NONE)) => NONE) stmts
-          );
-      in print_module module_name' content end;
-    fun write_module width (SOME destination) (modlname, content) =
+        val deresolve = deresolver module_name
+        fun print_import module_name = (semicolon o map str) ["import qualified", module_name];
+        val import_ps = import_includes_ps @ map (print_import o fst) imports;
+        fun print_stmt' gr name = case Graph.get_node gr name
+         of (_, NONE) => NONE
+          | (_, SOME stmt) => SOME (markup_stmt name (print_stmt deresolve (name, stmt)));
+        val body_ps = map_filter (print_stmt' gr) ((flat o rev o Graph.strong_conn) gr);
+      in
+        print_module_frame module_name
+          ((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps)
+      end;
+
+    (*serialization*)
+    fun write_module width (SOME destination) (module_name, content) =
           let
             val _ = File.check destination;
-            val filename = case modlname
-             of "" => Path.explode "Main.hs"
-              | _ => (Path.ext "hs" o Path.explode o implode o separate "/"
-                    o Long_Name.explode) modlname;
-            val pathname = Path.append destination filename;
-            val _ = File.mkdir_leaf (Path.dir pathname);
-          in File.write pathname
-            ("{-# OPTIONS_GHC -fglasgow-exts #-}\n\n"
-              ^ format [] width content)
+            val filepath = (Path.append destination o Path.ext "hs" o Path.explode o implode
+              o separate "/" o Long_Name.explode) module_name;
+            val _ = File.mkdir_leaf (Path.dir filepath);
+          in
+            (File.write filepath o format [] width o Pretty.chunks2)
+              [str "{-# OPTIONS_GHC -fglasgow-exts #-}", content]
           end
       | write_module width NONE (_, content) = writeln (format [] width content);
   in
     Code_Target.serialization
       (fn width => fn destination => K () o map (write_module width destination))
-      (fn present => fn width => rpair (fn _ => error "no deresolving") o format present width o Pretty.chunks o map snd)
-      (map (uncurry print_module) includes
-        @ map serialize_module (Symtab.dest hs_program))
+      (fn present => fn width => rpair (fn _ => error "no deresolving")
+        o format present width o Pretty.chunks o map snd)
+      (map (uncurry print_module_frame o apsnd single) includes
+        @ map (fn module_name => print_module module_name (Graph.get_node haskell_program module_name))
+          ((flat o rev o Graph.strong_conn) haskell_program))
   end;
 
 val serializer : Code_Target.serializer =
-  Code_Target.parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
+  Code_Target.parse_args (Scan.optional (Args.$$$ "root" -- Args.colon |-- Args.name) ""
     -- Scan.optional (Args.$$$ "string_classes" >> K true) false
     >> (fn (module_prefix, string_classes) =>
       serialize_haskell module_prefix string_classes));
diff -r 234e6ef4ff67 -r 202618462644 src/Tools/Code/code_namespace.ML
--- a/src/Tools/Code/code_namespace.ML	Tue Sep 07 14:11:05 2010 +0200
+++ b/src/Tools/Code/code_namespace.ML	Tue Sep 07 17:36:33 2010 +0200
@@ -6,12 +6,20 @@
 
 signature CODE_NAMESPACE =
 sig
-  val dest_name: string -> string * string
+  type flat_program
+  val flat_program: (string -> string) -> { module_alias: string -> string option,
+    module_prefix: string, reserved: Name.context, empty_nsp: 'a,
+    namify_stmt: Code_Thingol.stmt -> string -> 'a -> string * 'a,
+    modify_stmt: Code_Thingol.stmt -> Code_Thingol.stmt option }
+      -> Code_Thingol.program
+      -> { deresolver: string -> string -> string,
+           flat_program: flat_program }
+
   datatype ('a, 'b) node =
       Dummy
     | Stmt of 'a
     | Module of ('b * (string * ('a, 'b) node) Graph.T)
-  type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Graph.T
+  type ('a, 'b) hierarchical_program
   val hierarchical_program: (string -> string) -> { module_alias: string -> string option,
     reserved: Name.context, empty_nsp: 'c, namify_module: string -> 'c -> string * 'c,
     namify_stmt: Code_Thingol.stmt -> string -> 'c -> string * 'c,
@@ -29,11 +37,97 @@
 structure Code_Namespace : CODE_NAMESPACE =
 struct
 
-(** splitting names in module and base part **)
+(** building module name hierarchy **)
 
 val dest_name =
   apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
 
+fun build_module_namespace { module_alias, module_prefix, reserved } program =
+  let
+    fun alias_fragments name = case module_alias name
+     of SOME name' => Long_Name.explode name'
+      | NONE => map (fn name => fst (yield_singleton Name.variants name reserved))
+          (Long_Name.explode name);
+    val module_names = Graph.fold (insert (op =) o fst o dest_name o fst) program [];
+  in
+    fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ alias_fragments name))
+      module_names Symtab.empty
+  end;
+
+
+(** flat program structure **)
+
+type flat_program = ((string * Code_Thingol.stmt option) Graph.T * (string * string list) list) Graph.T;
+
+fun flat_program labelled_name { module_alias, module_prefix, reserved,
+      empty_nsp, namify_stmt, modify_stmt } program =
+  let
+
+    (* building module name hierarchy *)
+    val fragments_tab = build_module_namespace { module_alias = module_alias,
+      module_prefix = module_prefix, reserved = reserved } program;
+    val dest_name = dest_name
+      #>> (Long_Name.implode o the o Symtab.lookup fragments_tab);
+
+    (* distribute statements over hierarchy *)
+    fun add_stmt name stmt =
+      let
+        val (module_name, base) = dest_name name;
+      in
+        Graph.default_node (module_name, (Graph.empty, []))
+        #> (Graph.map_node module_name o apfst) (Graph.new_node (name, (base, stmt)))
+      end;
+    fun add_dependency name name' =
+      let
+        val (module_name, base) = dest_name name;
+        val (module_name', base') = dest_name name';
+      in if module_name = module_name'
+        then (Graph.map_node module_name o apfst) (Graph.add_edge (name, name'))
+        else (Graph.map_node module_name o apsnd) (AList.map_default (op =) (module_name', []) (insert (op =) name'))
+      end;
+    val proto_program = Graph.empty
+      |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
+      |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
+
+    (* name declarations and statement modifications *)
+    fun declare name (base, stmt) (gr, nsp) = 
+      let
+        val (base', nsp') = namify_stmt stmt base nsp;
+        val gr' = (Graph.map_node name o apfst) (K base') gr;
+      in (gr', nsp') end;
+    fun declarations gr = (gr, empty_nsp)
+      |> fold (fn name => declare name (Graph.get_node gr name)) (Graph.keys gr) 
+      |> fst
+      |> (Graph.map o K o apsnd) modify_stmt;
+    val flat_program = proto_program
+      |> (Graph.map o K o apfst) declarations;
+
+    (* qualified and unqualified imports, deresolving *)
+    fun base_deresolver name = fst (Graph.get_node
+      (fst (Graph.get_node flat_program (fst (dest_name name)))) name);
+    fun classify_names gr imports =
+      let
+        val import_tab = maps
+          (fn (module_name, names) => map (rpair module_name) names) imports;
+        val imported_names = map fst import_tab;
+        val here_names = Graph.keys gr;
+      in
+        Symtab.empty
+        |> fold (fn name => Symtab.update (name, base_deresolver name)) here_names
+        |> fold (fn name => Symtab.update (name,
+            Long_Name.append (the (AList.lookup (op =) import_tab name))
+              (base_deresolver name))) imported_names
+      end;
+    val name_tabs = AList.make (uncurry classify_names o Graph.get_node flat_program)
+      (Graph.keys flat_program);
+    val deresolver_tab = Symtab.empty
+      |> fold (fn (module_name, name_tab) => Symtab.update (module_name, name_tab)) name_tabs;
+    fun deresolver module_name name =
+      the (Symtab.lookup (the (Symtab.lookup deresolver_tab module_name)) name)
+      handle Option => error ("Unknown statement name: " ^ labelled_name name);
+
+  in { deresolver = deresolver, flat_program = flat_program } end;
+
 
 (** hierarchical program structure **)
 
@@ -56,13 +150,8 @@
   let
 
     (* building module name hierarchy *)
-    fun alias_fragments name = case module_alias name
-     of SOME name' => Long_Name.explode name'
-      | NONE => map (fn name => fst (yield_singleton Name.variants name reserved))
-          (Long_Name.explode name);
-    val module_names = Graph.fold (insert (op =) o fst o dest_name o fst) program [];
-    val fragments_tab = fold (fn name => Symtab.update
-      (name, alias_fragments name)) module_names Symtab.empty;
+    val fragments_tab = build_module_namespace { module_alias = module_alias,
+      module_prefix = "", reserved = reserved } program;
     val dest_name = dest_name #>> (the o Symtab.lookup fragments_tab);
 
     (* building empty module hierarchy *)
diff -r 234e6ef4ff67 -r 202618462644 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Tue Sep 07 14:11:05 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Tue Sep 07 17:36:33 2010 +0200
@@ -271,7 +271,6 @@
        of SOME (tyco, _) => Codegen.thyname_of_type thy tyco
         | NONE => Codegen.thyname_of_const thy c);
   fun purify_base "==>" = "follows"
-    | purify_base "op =" = "eq"
     | purify_base s = Name.desymbolize false s;
   fun namify thy get_basename get_thyname name =
     let