diff -r 5435ccdb4ea1 -r 08ec81dfc7fb doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML	Mon Nov 06 16:28:30 2006 +0100
@@ -0,0 +1,22 @@
+structure ROOT = 
+struct
+
+structure Nat = 
+struct
+
+datatype nat = Zero_nat | Suc of nat;
+
+end; (*struct Nat*)
+
+structure Codegen = 
+struct
+
+val dummy_set : Nat.nat -> Nat.nat list = Nat.Suc :: [];
+
+val foobar_set : Nat.nat list =
+  Nat.Zero_nat ::
+    (Nat.Suc Nat.Zero_nat :: (Nat.Suc (Nat.Suc Nat.Zero_nat) :: []));
+
+end; (*struct Codegen*)
+
+end; (*struct ROOT*)