doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML
changeset 22015 12b94d7f7e1f
parent 21993 4b802a9e0738
child 22386 4ebe883b02ff
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML	Fri Jan 05 14:30:08 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML	Fri Jan 05 14:31:44 2007 +0100
@@ -11,11 +11,11 @@
 structure Codegen = 
 struct
 
-val dummy_set : (Nat.nat -> Nat.nat) list = (Nat.Suc :: []);
+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) :: [])));
+  Nat.Zero_nat ::
+    (Nat.Suc Nat.Zero_nat :: (Nat.Suc (Nat.Suc Nat.Zero_nat) :: []));
 
 end; (*struct Codegen*)