# HG changeset patch
# User haftmann
# Date 1167927069 -3600
# Node ID 4b802a9e0738c5cbb43041988656a5ea23b582c5
# Parent  337990f42ce0a4fc6006653effd7115b45cde6b8
updated manual

diff -r 337990f42ce0 -r 4b802a9e0738 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Thu Jan 04 17:11:09 2007 +0100
@@ -182,7 +182,7 @@
 typedecl 'a foo
 
 definition
-  bar :: "'a foo \<Rightarrow> 'a \<Rightarrow> 'a"
+  bar :: "'a foo \<Rightarrow> 'a \<Rightarrow> 'a" where
   "bar x y = y"
 
 (*<*)
@@ -194,7 +194,7 @@
 datatype 'a foo = Foo
 
 definition
-  bar :: "'a foo \<Rightarrow> 'a \<Rightarrow> 'a"
+  bar :: "'a foo \<Rightarrow> 'a \<Rightarrow> 'a" where
   "bar x y = y"
 (*>*)
 
@@ -212,7 +212,7 @@
 (*>*)
 
 definition
-  pick_some :: "'a list \<Rightarrow> 'a"
+  pick_some :: "'a list \<Rightarrow> 'a" where
   "pick_some xs = (SOME x. x \<in> set xs)"
 
 (*<*)
@@ -221,7 +221,7 @@
 setup {* Sign.parent_path *}
 
 definition
-  pick_some :: "'a list \<Rightarrow> 'a"
+  pick_some :: "'a list \<Rightarrow> 'a" where
   "pick_some = hd"
 (*>*)
 
@@ -655,7 +655,7 @@
 *}
 
 definition
-  double_inc :: "int \<Rightarrow> int"
+  double_inc :: "int \<Rightarrow> int" where
   "double_inc k = 2 * k + 1"
 
 code_gen double_inc (SML "examples/integers.ML")
@@ -745,11 +745,11 @@
 (*>*)
 
 axclass eq \<subseteq> type
-  attach "op ="
+  (attach "op =")
 
 text {*
   This merely introduces a class @{text eq} with corresponding
-  operation @{const "op ="};
+  operation @{text "op ="};
   the preprocessing framework does the rest.
 *}
 
@@ -926,7 +926,7 @@
   (SML "![]" and infixl 7 "::")
 
 definition
-  dummy_set :: "(nat \<Rightarrow> nat) set"
+  dummy_set :: "(nat \<Rightarrow> nat) set" where
   "dummy_set = {Suc}"
 
 text {*
@@ -946,7 +946,7 @@
 *}
 
 definition
-  foobar_set :: "nat set"
+  foobar_set :: "nat set" where
   "foobar_set = {0, 1, 2}"
 
 text {*
@@ -1053,7 +1053,7 @@
 *}
 
 definition
-  arbitrary_option :: "'a option"
+  arbitrary_option :: "'a option" where
   [symmetric, code inline]: "arbitrary_option = arbitrary"
 
 text {*
diff -r 337990f42ce0 -r 4b802a9e0738 doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Thu Jan 04 17:11:09 2007 +0100
@@ -225,7 +225,7 @@
 \isanewline
 \isacommand{definition}\isamarkupfalse%
 \isanewline
-\ \ bar\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ foo\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
+\ \ bar\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ foo\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
 \ \ {\isachardoublequoteopen}bar\ x\ y\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
 %
 \isadelimML
@@ -266,7 +266,7 @@
 \endisadelimML
 \isacommand{definition}\isamarkupfalse%
 \isanewline
-\ \ pick{\isacharunderscore}some\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
+\ \ pick{\isacharunderscore}some\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
 \ \ {\isachardoublequoteopen}pick{\isacharunderscore}some\ xs\ {\isacharequal}\ {\isacharparenleft}SOME\ x{\isachardot}\ x\ {\isasymin}\ set\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
 %
 \isadelimML
@@ -864,7 +864,7 @@
 \isamarkuptrue%
 \isacommand{definition}\isamarkupfalse%
 \isanewline
-\ \ double{\isacharunderscore}inc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\isanewline
+\ \ double{\isacharunderscore}inc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
 \ \ {\isachardoublequoteopen}double{\isacharunderscore}inc\ k\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ k\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
 \isanewline
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
@@ -981,7 +981,7 @@
 \isanewline
 \isacommand{axclass}\isamarkupfalse%
 \ eq\ {\isasymsubseteq}\ type\isanewline
-\ \ \isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}%
+\ \ {\isacharparenleft}\isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
 \begin{isamarkuptext}%
 This merely introduces a class \isa{eq} with corresponding
   operation \isa{foo{\isachardot}op\ {\isacharequal}};
@@ -1351,7 +1351,7 @@
 \isanewline
 \isacommand{definition}\isamarkupfalse%
 \isanewline
-\ \ dummy{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ set{\isachardoublequoteclose}\isanewline
+\ \ dummy{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ set{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
 \ \ {\isachardoublequoteopen}dummy{\isacharunderscore}set\ {\isacharequal}\ {\isacharbraceleft}Suc{\isacharbraceright}{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 Then code generation for \isa{dummy{\isacharunderscore}set} will fail.
@@ -1371,7 +1371,7 @@
 \isamarkuptrue%
 \isacommand{definition}\isamarkupfalse%
 \isanewline
-\ \ foobar{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
+\ \ foobar{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
 \ \ {\isachardoublequoteopen}foobar{\isacharunderscore}set\ {\isacharequal}\ {\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 In this case the serializer would complain that \isa{insert}
@@ -1513,7 +1513,7 @@
 \isamarkuptrue%
 \isacommand{definition}\isamarkupfalse%
 \isanewline
-\ \ arbitrary{\isacharunderscore}option\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ option{\isachardoublequoteclose}\isanewline
+\ \ arbitrary{\isacharunderscore}option\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ option{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
 \ \ {\isacharbrackleft}symmetric{\isacharcomma}\ code\ inline{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}arbitrary{\isacharunderscore}option\ {\isacharequal}\ arbitrary{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 By that, we replace any \isa{arbitrary} with option type
diff -r 337990f42ce0 -r 4b802a9e0738 doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Thu Jan 04 17:11:09 2007 +0100
@@ -2,11 +2,10 @@
 import qualified Nat
 
 class Null a where
-  null :: a
+  nulla :: a
 
-head :: (Codegen.Null a_1) => [a_1] -> a_1
-head (y : xs) = y
-head [] = Codegen.null
+heada :: (Codegen.Null a) => ([a] -> a)
+heada (y : xs) = y
 
 null_option :: Maybe b
 null_option = Nothing
@@ -15,4 +14,4 @@
   null = Codegen.null_option
 
 dummy :: Maybe Nat.Nat
-dummy = Codegen.head [Just (Nat.Suc Nat.Zero_nat), Nothing]
+dummy = Codegen.heada [Just (Nat.Suc Nat.Zero_nat), Nothing]
diff -r 337990f42ce0 -r 4b802a9e0738 doc-src/IsarAdvanced/Codegen/Thy/examples/arbitrary.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/arbitrary.ML	Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/arbitrary.ML	Thu Jan 04 17:11:09 2007 +0100
@@ -6,8 +6,7 @@
 
 val arbitrary_option : 'a option = NONE;
 
-fun dummy_option [] = arbitrary_option
-  | dummy_option (x :: xs) = SOME x;
+fun dummy_option [] = arbitrary_option;
 
 end; (*struct Codegen*)
 
diff -r 337990f42ce0 -r 4b802a9e0738 doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML	Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML	Thu Jan 04 17:11:09 2007 +0100
@@ -4,8 +4,7 @@
 structure HOL = 
 struct
 
-fun nota false = true
-  | nota true = false;
+fun nota false = true;
 
 end; (*struct HOL*)
 
@@ -14,9 +13,7 @@
 
 datatype nat = Zero_nat | Suc of nat;
 
-fun less_nat Zero_nat (Suc n) = true
-  | less_nat n Zero_nat = false
-  | less_nat (Suc m) (Suc n) = less_nat m n;
+fun less_nat Zero_nat (Suc n) = true;
 
 fun less_eq_nat m n = HOL.nota (less_nat n m);
 
@@ -25,7 +22,9 @@
 structure Codegen = 
 struct
 
-fun in_interval (k, l) n = Nat.less_eq_nat k n andalso Nat.less_eq_nat n l;
+fun in_interval (k, l) n = (Nat.less_eq_nat k n andalso Nat.less_eq_nat n l)
+  | in_interval (k, l) n =
+    (Nat.less_eq_nat k n andalso Nat.less_eq_nat n l);
 
 end; (*struct Codegen*)
 
diff -r 337990f42ce0 -r 4b802a9e0738 doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML	Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML	Thu Jan 04 17:11:09 2007 +0100
@@ -6,13 +6,9 @@
 
 datatype boola = True | False;
 
-fun nota False = True
-  | nota True = False;
+fun nota False = True;
 
-fun op_conj y True = y
-  | op_conj x False = False
-  | op_conj True y = y
-  | op_conj False x = False;
+fun op_conj y True = y;
 
 end; (*struct HOL*)
 
@@ -21,9 +17,7 @@
 
 datatype nat = Zero_nat | Suc of nat;
 
-fun less_nat Zero_nat (Suc n) = HOL.True
-  | less_nat n Zero_nat = HOL.False
-  | less_nat (Suc m) (Suc n) = less_nat m n;
+fun less_nat Zero_nat (Suc n) = HOL.True;
 
 fun less_eq_nat m n = HOL.nota (less_nat n m);
 
@@ -33,7 +27,9 @@
 struct
 
 fun in_interval (k, l) n =
-  HOL.op_conj (Nat.less_eq_nat k n) (Nat.less_eq_nat n l);
+  HOL.op_conj (Nat.less_eq_nat k n) (Nat.less_eq_nat n l)
+  | in_interval (k, l) n =
+    HOL.op_conj (Nat.less_eq_nat k n) (Nat.less_eq_nat n l);
 
 end; (*struct Codegen*)
 
diff -r 337990f42ce0 -r 4b802a9e0738 doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML	Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML	Thu Jan 04 17:11:09 2007 +0100
@@ -4,8 +4,7 @@
 structure HOL = 
 struct
 
-fun nota false = true
-  | nota true = false;
+fun nota false = true;
 
 end; (*struct HOL*)
 
@@ -14,9 +13,7 @@
 
 datatype nat = Zero_nat | Suc of nat;
 
-fun less_nat Zero_nat (Suc n) = true
-  | less_nat n Zero_nat = false
-  | less_nat (Suc m) (Suc n) = less_nat m n;
+fun less_nat Zero_nat (Suc n) = true;
 
 fun less_eq_nat m n = HOL.nota (less_nat n m);
 
@@ -26,7 +23,9 @@
 struct
 
 fun in_interval (k, l) n =
-  (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l);
+  (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l)
+  | in_interval (k, l) n =
+    (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l);
 
 end; (*struct Codegen*)
 
diff -r 337990f42ce0 -r 4b802a9e0738 doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Thu Jan 04 17:11:09 2007 +0100
@@ -14,12 +14,11 @@
 type 'a null = {null_ : 'a};
 fun null (A_:'a null) = #null_ A_;
 
-fun head (A_1_:'a_1 null) (y :: xs) = y
-  | head (A_1_:'a_1 null) [] = null A_1_;
+fun head (A_:'a null) (y :: xs) = y;
 
 val null_option : 'b option = NONE;
 
-fun null_optiona () = {null_ = null_option} : ('b option) null
+fun null_optiona () = {null_ = null_option} : ('b option) null ;;
 
 val dummy : Nat.nat option =
   head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
diff -r 337990f42ce0 -r 4b802a9e0738 doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Thu Jan 04 17:11:09 2007 +0100
@@ -12,9 +12,8 @@
 structure List = 
 struct
 
-fun memberl (A_1_:'a_1 Code_Generator.eq) x (y :: ys) =
-  Code_Generator.op_eq A_1_ x y orelse memberl A_1_ x ys
-  | memberl (A_1_:'a_1 Code_Generator.eq) x [] = false;
+fun memberl (A_:'a Code_Generator.eq) x (y :: ys) =
+  (Code_Generator.op_eq A_ x y orelse memberl A_ x ys);
 
 end; (*struct List*)
 
@@ -25,8 +24,7 @@
   (if List.memberl A_ z xs
     then (if List.memberl A_ z ys then collect_duplicates A_ xs ys zs
            else collect_duplicates A_ xs (z :: ys) zs)
-    else collect_duplicates A_ (z :: xs) (z :: ys) zs)
-  | collect_duplicates (A_:'a Code_Generator.eq) y ys [] = y;
+    else collect_duplicates A_ (z :: xs) (z :: ys) zs);
 
 end; (*struct Codegen*)
 
diff -r 337990f42ce0 -r 4b802a9e0738 doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML	Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML	Thu Jan 04 17:11:09 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*)
 
diff -r 337990f42ce0 -r 4b802a9e0738 doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Thu Jan 04 17:11:09 2007 +0100
@@ -7,18 +7,16 @@
 datatype nat = Zero_nat | Suc of nat;
 
 fun plus_nat (Suc m) n = plus_nat m (Suc n)
-  | plus_nat Zero_nat y = y;
+  | plus_nat (Suc m) n = Suc (plus_nat m n);
 
-fun times_nat (Suc m) n = plus_nat n (times_nat m n)
-  | times_nat Zero_nat n = Zero_nat;
+fun times_nat (Suc m) n = plus_nat n (times_nat m n);
 
 end; (*struct Nat*)
 
 structure Codegen = 
 struct
 
-fun fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n)
-  | fac Nat.Zero_nat = Nat.Suc Nat.Zero_nat;
+fun fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n);
 
 end; (*struct Codegen*)
 
diff -r 337990f42ce0 -r 4b802a9e0738 doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML	Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML	Thu Jan 04 17:11:09 2007 +0100
@@ -7,10 +7,9 @@
 datatype nat = Zero_nat | Suc of nat;
 
 fun plus_nat (Suc m) n = plus_nat m (Suc n)
-  | plus_nat Zero_nat y = y;
+  | plus_nat (Suc m) n = Suc (plus_nat m n);
 
-fun times_nat (Suc m) n = plus_nat n (times_nat m n)
-  | times_nat Zero_nat n = Zero_nat;
+fun times_nat (Suc m) n = plus_nat n (times_nat m n);
 
 end; (*struct Nat*)
 
@@ -19,7 +18,8 @@
 
 fun fac n =
   (case n of Nat.Zero_nat => Nat.Suc Nat.Zero_nat
-     | Nat.Suc ma => Nat.times_nat n (fac ma));
+     | Nat.Suc m => Nat.times_nat n (fac m))
+  | fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n);
 
 end; (*struct Codegen*)
 
diff -r 337990f42ce0 -r 4b802a9e0738 doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML	Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML	Thu Jan 04 17:11:09 2007 +0100
@@ -4,8 +4,8 @@
 structure Codegen = 
 struct
 
-fun double_inc a =
-  IntInf.+ ((IntInf.* ((2 : IntInf.int), a)), (1 : IntInf.int));
+val double_inc : IntInf.int -> IntInf.int =
+  (fn k => IntInf.+ ((IntInf.* ((2 : IntInf.int), k)), (1 : IntInf.int)));
 
 end; (*struct Codegen*)
 
diff -r 337990f42ce0 -r 4b802a9e0738 doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML	Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML	Thu Jan 04 17:11:09 2007 +0100
@@ -14,7 +14,7 @@
 
 fun op_eq_prod (A_:'a Code_Generator.eq) (B_:'b Code_Generator.eq) (x1, y1)
   (x2, y2) =
-  Code_Generator.op_eq A_ x1 x2 andalso Code_Generator.op_eq B_ y1 y2;
+  (Code_Generator.op_eq A_ x1 x2 andalso Code_Generator.op_eq B_ y1 y2);
 
 end; (*struct Product_Type*)
 
@@ -33,18 +33,18 @@
 fun less_prod (B_:'b Code_Generator.eq * 'b Orderings.ord)
   (C_:'c Code_Generator.eq * 'c Orderings.ord) p1 p2 =
   let
-    val (x1a, y1a) = p1;
-    val (x2a, y2a) = p2;
+    val (x1, y1) = p1;
+    val (x2, y2) = p2;
   in
-    Orderings.less (#2 B_) x1a x2a orelse
-      Code_Generator.op_eq (#1 B_) x1a x2a andalso
-        Orderings.less (#2 C_) y1a y2a
+    (Orderings.less (#2 B_) x1 x2 orelse
+      Code_Generator.op_eq (#1 B_) x1 x2 andalso
+        Orderings.less (#2 C_) y1 y2)
   end;
 
 fun less_eq_prod (B_:'b Code_Generator.eq * 'b Orderings.ord)
   (C_:'c Code_Generator.eq * 'c Orderings.ord) p1 p2 =
-  less_prod ((#1 B_), (#2 B_)) ((#1 C_), (#2 C_)) p1 p2 orelse
-    Product_Type.op_eq_prod (#1 B_) (#1 C_) p1 p2;
+  (less_prod ((#1 B_), (#2 B_)) ((#1 C_), (#2 C_)) p1 p2 orelse
+    Product_Type.op_eq_prod (#1 B_) (#1 C_) p1 p2);
 
 end; (*struct Codegen*)
 
diff -r 337990f42ce0 -r 4b802a9e0738 doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML	Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML	Thu Jan 04 17:11:09 2007 +0100
@@ -5,8 +5,7 @@
 struct
 
 fun lookup ((k, v) :: xs) l =
-  (if ((k : string) = l) then SOME v else lookup xs l)
-  | lookup [] l = NONE;
+  (if ((k : string) = l) then SOME v else lookup xs l);
 
 end; (*struct Codegen*)
 
diff -r 337990f42ce0 -r 4b802a9e0738 doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Thu Jan 04 17:11:09 2007 +0100
@@ -6,13 +6,9 @@
 
 datatype nat = Zero_nat | Suc of nat;
 
-fun less_nat Zero_nat (Suc n) = true
-  | less_nat n Zero_nat = false
-  | less_nat (Suc m) (Suc n) = less_nat m n;
+fun less_nat Zero_nat (Suc n) = true;
 
-fun minus_nat (Suc m) (Suc n) = minus_nat m n
-  | minus_nat Zero_nat n = Zero_nat
-  | minus_nat y Zero_nat = y;
+fun minus_nat (Suc m) (Suc n) = minus_nat m n;
 
 end; (*struct Nat*)
 
@@ -20,13 +16,7 @@
 struct
 
 fun pick ((k, v) :: xs) n =
-  (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k))
-  | pick (x :: xs) n =
-    let
-      val (ka, va) = x;
-    in
-      (if Nat.less_nat n ka then va else pick xs (Nat.minus_nat n ka))
-    end;
+  (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k));
 
 end; (*struct Codegen*)
 
diff -r 337990f42ce0 -r 4b802a9e0738 doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML	Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML	Thu Jan 04 17:11:09 2007 +0100
@@ -6,13 +6,9 @@
 
 datatype nat = Zero_nat | Suc of nat;
 
-fun less_nat Zero_nat (Suc n) = true
-  | less_nat n Zero_nat = false
-  | less_nat (Suc m) (Suc n) = less_nat m n;
+fun less_nat Zero_nat (Suc n) = true;
 
-fun minus_nat (Suc m) (Suc n) = minus_nat m n
-  | minus_nat Zero_nat n = Zero_nat
-  | minus_nat y Zero_nat = y;
+fun minus_nat (Suc m) (Suc n) = minus_nat m n;
 
 end; (*struct Nat*)