*** empty log message ***

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML	Fri May 25 21:08:45 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML	Fri May 25 21:08:46 2007 +0200
@@ -6,10 +6,10 @@
 
 datatype boola = True | False;
 
-fun op_and x True = x
-  | op_and x False = False
-  | op_and True x = x
-  | op_and False x = False;
+fun anda x True = x
+  | anda x False = False
+  | anda True x = x
+  | anda False x = False;
 
 end; (*struct HOL*)
 
@@ -29,7 +29,7 @@
 struct
 
 fun in_interval (k, l) n =
-  HOL.op_and (Nat.less_eq_nat k n) (Nat.less_eq_nat n l);
+  HOL.anda (Nat.less_eq_nat k n) (Nat.less_eq_nat n l);
 
 end; (*struct Codegen*)
 

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Fri May 25 21:08:45 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Fri May 25 21:08:46 2007 +0200
@@ -4,8 +4,8 @@
 structure Code_Generator = 
 struct
 
-type 'a eq = {op_eq : 'a -> 'a -> bool};
-fun op_eq (A_:'a eq) = #op_eq A_;
+type 'a eq = {eq : 'a -> 'a -> bool};
+fun eq (A_:'a eq) = #eq A_;
 
 end; (*struct Code_Generator*)
 
@@ -13,7 +13,7 @@
 struct
 
 fun memberl A_ x (y :: ys) =
-  Code_Generator.op_eq A_ x y orelse memberl A_ x ys
+  Code_Generator.eq A_ x y orelse memberl A_ x ys
   | memberl A_ x [] = false;
 
 end; (*struct List*)

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML	Fri May 25 21:08:45 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML	Fri May 25 21:08:46 2007 +0200
@@ -13,17 +13,17 @@
 structure Code_Generator = 
 struct
 
-type 'a eq = {op_eq : 'a -> 'a -> bool};
-fun op_eq (A_:'a eq) = #op_eq A_;
+type 'a eq = {eq : 'a -> 'a -> bool};
+fun eq (A_:'a eq) = #eq A_;
 
 end; (*struct Code_Generator*)
 
 structure Codegen = 
 struct
 
-fun less_eq_times (A1_, A2_) B_ (x1, y1) (x2, y2) =
+fun less_eq_product (A1_, A2_) B_ (x1, y1) (x2, y2) =
   Orderings.less A2_ x1 x2 orelse
-    Code_Generator.op_eq A1_ x1 x2 andalso Orderings.less_eq B_ y1 y2;
+    Code_Generator.eq A1_ x1 x2 andalso Orderings.less_eq B_ y1 y2;
 
 end; (*struct Codegen*)
 

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML	Fri May 25 21:08:45 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML	Fri May 25 21:08:46 2007 +0200
@@ -6,21 +6,21 @@
 
 datatype nat = Zero_nat | Suc of nat;
 
+fun eq_nat Zero_nat (Suc m) = false
+  | eq_nat (Suc n) Zero_nat = false
+  | eq_nat (Suc n) (Suc m) = eq_nat n m
+  | eq_nat Zero_nat Zero_nat = true;
+
 fun plus_nat (Suc m) n = plus_nat m (Suc n)
   | plus_nat Zero_nat n = n;
 
-fun op_eq_nat Zero_nat (Suc m) = false
-  | op_eq_nat (Suc n) Zero_nat = false
-  | op_eq_nat (Suc n) (Suc m) = op_eq_nat n m
-  | op_eq_nat Zero_nat Zero_nat = true;
-
 end; (*struct Nat*)
 
 structure Code_Generator = 
 struct
 
-type 'a eq = {op_eq : 'a -> 'a -> bool};
-fun op_eq (A_:'a eq) = #op_eq A_;
+type 'a eq = {eq : 'a -> 'a -> bool};
+fun eq (A_:'a eq) = #eq A_;
 
 end; (*struct Code_Generator*)
 
@@ -40,267 +40,273 @@
 fun null (x :: xs) = false
   | null [] = true;
 
-fun op_eq_nibble Nibble0 Nibble0 = true
-  | op_eq_nibble Nibble1 Nibble1 = true
-  | op_eq_nibble Nibble2 Nibble2 = true
-  | op_eq_nibble Nibble3 Nibble3 = true
-  | op_eq_nibble Nibble4 Nibble4 = true
-  | op_eq_nibble Nibble5 Nibble5 = true
-  | op_eq_nibble Nibble6 Nibble6 = true
-  | op_eq_nibble Nibble7 Nibble7 = true
-  | op_eq_nibble Nibble8 Nibble8 = true
-  | op_eq_nibble Nibble9 Nibble9 = true
-  | op_eq_nibble NibbleA NibbleA = true
-  | op_eq_nibble NibbleB NibbleB = true
-  | op_eq_nibble NibbleC NibbleC = true
-  | op_eq_nibble NibbleD NibbleD = true
-  | op_eq_nibble NibbleE NibbleE = true
-  | op_eq_nibble NibbleF NibbleF = true
-  | op_eq_nibble Nibble0 Nibble1 = false
-  | op_eq_nibble Nibble0 Nibble2 = false
-  | op_eq_nibble Nibble0 Nibble3 = false
-  | op_eq_nibble Nibble0 Nibble4 = false
-  | op_eq_nibble Nibble0 Nibble5 = false
-  | op_eq_nibble Nibble0 Nibble6 = false
-  | op_eq_nibble Nibble0 Nibble7 = false
-  | op_eq_nibble Nibble0 Nibble8 = false
-  | op_eq_nibble Nibble0 Nibble9 = false
-  | op_eq_nibble Nibble0 NibbleA = false
-  | op_eq_nibble Nibble0 NibbleB = false
-  | op_eq_nibble Nibble0 NibbleC = false
-  | op_eq_nibble Nibble0 NibbleD = false
-  | op_eq_nibble Nibble0 NibbleE = false
-  | op_eq_nibble Nibble0 NibbleF = false
-  | op_eq_nibble Nibble1 Nibble2 = false
-  | op_eq_nibble Nibble1 Nibble3 = false
-  | op_eq_nibble Nibble1 Nibble4 = false
-  | op_eq_nibble Nibble1 Nibble5 = false
-  | op_eq_nibble Nibble1 Nibble6 = false
-  | op_eq_nibble Nibble1 Nibble7 = false
-  | op_eq_nibble Nibble1 Nibble8 = false
-  | op_eq_nibble Nibble1 Nibble9 = false
-  | op_eq_nibble Nibble1 NibbleA = false
-  | op_eq_nibble Nibble1 NibbleB = false
-  | op_eq_nibble Nibble1 NibbleC = false
-  | op_eq_nibble Nibble1 NibbleD = false
-  | op_eq_nibble Nibble1 NibbleE = false
-  | op_eq_nibble Nibble1 NibbleF = false
-  | op_eq_nibble Nibble2 Nibble3 = false
-  | op_eq_nibble Nibble2 Nibble4 = false
-  | op_eq_nibble Nibble2 Nibble5 = false
-  | op_eq_nibble Nibble2 Nibble6 = false
-  | op_eq_nibble Nibble2 Nibble7 = false
-  | op_eq_nibble Nibble2 Nibble8 = false
-  | op_eq_nibble Nibble2 Nibble9 = false
-  | op_eq_nibble Nibble2 NibbleA = false
-  | op_eq_nibble Nibble2 NibbleB = false
-  | op_eq_nibble Nibble2 NibbleC = false
-  | op_eq_nibble Nibble2 NibbleD = false
-  | op_eq_nibble Nibble2 NibbleE = false
-  | op_eq_nibble Nibble2 NibbleF = false
-  | op_eq_nibble Nibble3 Nibble4 = false
-  | op_eq_nibble Nibble3 Nibble5 = false
-  | op_eq_nibble Nibble3 Nibble6 = false
-  | op_eq_nibble Nibble3 Nibble7 = false
-  | op_eq_nibble Nibble3 Nibble8 = false
-  | op_eq_nibble Nibble3 Nibble9 = false
-  | op_eq_nibble Nibble3 NibbleA = false
-  | op_eq_nibble Nibble3 NibbleB = false
-  | op_eq_nibble Nibble3 NibbleC = false
-  | op_eq_nibble Nibble3 NibbleD = false
-  | op_eq_nibble Nibble3 NibbleE = false
-  | op_eq_nibble Nibble3 NibbleF = false
-  | op_eq_nibble Nibble4 Nibble5 = false
-  | op_eq_nibble Nibble4 Nibble6 = false
-  | op_eq_nibble Nibble4 Nibble7 = false
-  | op_eq_nibble Nibble4 Nibble8 = false
-  | op_eq_nibble Nibble4 Nibble9 = false
-  | op_eq_nibble Nibble4 NibbleA = false
-  | op_eq_nibble Nibble4 NibbleB = false
-  | op_eq_nibble Nibble4 NibbleC = false
-  | op_eq_nibble Nibble4 NibbleD = false
-  | op_eq_nibble Nibble4 NibbleE = false
-  | op_eq_nibble Nibble4 NibbleF = false
-  | op_eq_nibble Nibble5 Nibble6 = false
-  | op_eq_nibble Nibble5 Nibble7 = false
-  | op_eq_nibble Nibble5 Nibble8 = false
-  | op_eq_nibble Nibble5 Nibble9 = false
-  | op_eq_nibble Nibble5 NibbleA = false
-  | op_eq_nibble Nibble5 NibbleB = false
-  | op_eq_nibble Nibble5 NibbleC = false
-  | op_eq_nibble Nibble5 NibbleD = false
-  | op_eq_nibble Nibble5 NibbleE = false
-  | op_eq_nibble Nibble5 NibbleF = false
-  | op_eq_nibble Nibble6 Nibble7 = false
-  | op_eq_nibble Nibble6 Nibble8 = false
-  | op_eq_nibble Nibble6 Nibble9 = false
-  | op_eq_nibble Nibble6 NibbleA = false
-  | op_eq_nibble Nibble6 NibbleB = false
-  | op_eq_nibble Nibble6 NibbleC = false
-  | op_eq_nibble Nibble6 NibbleD = false
-  | op_eq_nibble Nibble6 NibbleE = false
-  | op_eq_nibble Nibble6 NibbleF = false
-  | op_eq_nibble Nibble7 Nibble8 = false
-  | op_eq_nibble Nibble7 Nibble9 = false
-  | op_eq_nibble Nibble7 NibbleA = false
-  | op_eq_nibble Nibble7 NibbleB = false
-  | op_eq_nibble Nibble7 NibbleC = false
-  | op_eq_nibble Nibble7 NibbleD = false
-  | op_eq_nibble Nibble7 NibbleE = false
-  | op_eq_nibble Nibble7 NibbleF = false
-  | op_eq_nibble Nibble8 Nibble9 = false
-  | op_eq_nibble Nibble8 NibbleA = false
-  | op_eq_nibble Nibble8 NibbleB = false
-  | op_eq_nibble Nibble8 NibbleC = false
-  | op_eq_nibble Nibble8 NibbleD = false
-  | op_eq_nibble Nibble8 NibbleE = false
-  | op_eq_nibble Nibble8 NibbleF = false
-  | op_eq_nibble Nibble9 NibbleA = false
-  | op_eq_nibble Nibble9 NibbleB = false
-  | op_eq_nibble Nibble9 NibbleC = false
-  | op_eq_nibble Nibble9 NibbleD = false
-  | op_eq_nibble Nibble9 NibbleE = false
-  | op_eq_nibble Nibble9 NibbleF = false
-  | op_eq_nibble NibbleA NibbleB = false
-  | op_eq_nibble NibbleA NibbleC = false
-  | op_eq_nibble NibbleA NibbleD = false
-  | op_eq_nibble NibbleA NibbleE = false
-  | op_eq_nibble NibbleA NibbleF = false
-  | op_eq_nibble NibbleB NibbleC = false
-  | op_eq_nibble NibbleB NibbleD = false
-  | op_eq_nibble NibbleB NibbleE = false
-  | op_eq_nibble NibbleB NibbleF = false
-  | op_eq_nibble NibbleC NibbleD = false
-  | op_eq_nibble NibbleC NibbleE = false
-  | op_eq_nibble NibbleC NibbleF = false
-  | op_eq_nibble NibbleD NibbleE = false
-  | op_eq_nibble NibbleD NibbleF = false
-  | op_eq_nibble NibbleE NibbleF = false
-  | op_eq_nibble Nibble1 Nibble0 = false
-  | op_eq_nibble Nibble2 Nibble0 = false
-  | op_eq_nibble Nibble3 Nibble0 = false
-  | op_eq_nibble Nibble4 Nibble0 = false
-  | op_eq_nibble Nibble5 Nibble0 = false
-  | op_eq_nibble Nibble6 Nibble0 = false
-  | op_eq_nibble Nibble7 Nibble0 = false
-  | op_eq_nibble Nibble8 Nibble0 = false
-  | op_eq_nibble Nibble9 Nibble0 = false
-  | op_eq_nibble NibbleA Nibble0 = false
-  | op_eq_nibble NibbleB Nibble0 = false
-  | op_eq_nibble NibbleC Nibble0 = false
-  | op_eq_nibble NibbleD Nibble0 = false
-  | op_eq_nibble NibbleE Nibble0 = false
-  | op_eq_nibble NibbleF Nibble0 = false
-  | op_eq_nibble Nibble2 Nibble1 = false
-  | op_eq_nibble Nibble3 Nibble1 = false
-  | op_eq_nibble Nibble4 Nibble1 = false
-  | op_eq_nibble Nibble5 Nibble1 = false
-  | op_eq_nibble Nibble6 Nibble1 = false
-  | op_eq_nibble Nibble7 Nibble1 = false
-  | op_eq_nibble Nibble8 Nibble1 = false
-  | op_eq_nibble Nibble9 Nibble1 = false
-  | op_eq_nibble NibbleA Nibble1 = false
-  | op_eq_nibble NibbleB Nibble1 = false
-  | op_eq_nibble NibbleC Nibble1 = false
-  | op_eq_nibble NibbleD Nibble1 = false
-  | op_eq_nibble NibbleE Nibble1 = false
-  | op_eq_nibble NibbleF Nibble1 = false
-  | op_eq_nibble Nibble3 Nibble2 = false
-  | op_eq_nibble Nibble4 Nibble2 = false
-  | op_eq_nibble Nibble5 Nibble2 = false
-  | op_eq_nibble Nibble6 Nibble2 = false
-  | op_eq_nibble Nibble7 Nibble2 = false
-  | op_eq_nibble Nibble8 Nibble2 = false
-  | op_eq_nibble Nibble9 Nibble2 = false
-  | op_eq_nibble NibbleA Nibble2 = false
-  | op_eq_nibble NibbleB Nibble2 = false
-  | op_eq_nibble NibbleC Nibble2 = false
-  | op_eq_nibble NibbleD Nibble2 = false
-  | op_eq_nibble NibbleE Nibble2 = false
-  | op_eq_nibble NibbleF Nibble2 = false
-  | op_eq_nibble Nibble4 Nibble3 = false
-  | op_eq_nibble Nibble5 Nibble3 = false
-  | op_eq_nibble Nibble6 Nibble3 = false
-  | op_eq_nibble Nibble7 Nibble3 = false
-  | op_eq_nibble Nibble8 Nibble3 = false
-  | op_eq_nibble Nibble9 Nibble3 = false
-  | op_eq_nibble NibbleA Nibble3 = false
-  | op_eq_nibble NibbleB Nibble3 = false
-  | op_eq_nibble NibbleC Nibble3 = false
-  | op_eq_nibble NibbleD Nibble3 = false
-  | op_eq_nibble NibbleE Nibble3 = false
-  | op_eq_nibble NibbleF Nibble3 = false
-  | op_eq_nibble Nibble5 Nibble4 = false
-  | op_eq_nibble Nibble6 Nibble4 = false
-  | op_eq_nibble Nibble7 Nibble4 = false
-  | op_eq_nibble Nibble8 Nibble4 = false
-  | op_eq_nibble Nibble9 Nibble4 = false
-  | op_eq_nibble NibbleA Nibble4 = false
-  | op_eq_nibble NibbleB Nibble4 = false
-  | op_eq_nibble NibbleC Nibble4 = false
-  | op_eq_nibble NibbleD Nibble4 = false
-  | op_eq_nibble NibbleE Nibble4 = false
-  | op_eq_nibble NibbleF Nibble4 = false
-  | op_eq_nibble Nibble6 Nibble5 = false
-  | op_eq_nibble Nibble7 Nibble5 = false
-  | op_eq_nibble Nibble8 Nibble5 = false
-  | op_eq_nibble Nibble9 Nibble5 = false
-  | op_eq_nibble NibbleA Nibble5 = false
-  | op_eq_nibble NibbleB Nibble5 = false
-  | op_eq_nibble NibbleC Nibble5 = false
-  | op_eq_nibble NibbleD Nibble5 = false
-  | op_eq_nibble NibbleE Nibble5 = false
-  | op_eq_nibble NibbleF Nibble5 = false
-  | op_eq_nibble Nibble7 Nibble6 = false
-  | op_eq_nibble Nibble8 Nibble6 = false
-  | op_eq_nibble Nibble9 Nibble6 = false
-  | op_eq_nibble NibbleA Nibble6 = false
-  | op_eq_nibble NibbleB Nibble6 = false
-  | op_eq_nibble NibbleC Nibble6 = false
-  | op_eq_nibble NibbleD Nibble6 = false
-  | op_eq_nibble NibbleE Nibble6 = false
-  | op_eq_nibble NibbleF Nibble6 = false
-  | op_eq_nibble Nibble8 Nibble7 = false
-  | op_eq_nibble Nibble9 Nibble7 = false
-  | op_eq_nibble NibbleA Nibble7 = false
-  | op_eq_nibble NibbleB Nibble7 = false
-  | op_eq_nibble NibbleC Nibble7 = false
-  | op_eq_nibble NibbleD Nibble7 = false
-  | op_eq_nibble NibbleE Nibble7 = false
-  | op_eq_nibble NibbleF Nibble7 = false
-  | op_eq_nibble Nibble9 Nibble8 = false
-  | op_eq_nibble NibbleA Nibble8 = false
-  | op_eq_nibble NibbleB Nibble8 = false
-  | op_eq_nibble NibbleC Nibble8 = false
-  | op_eq_nibble NibbleD Nibble8 = false
-  | op_eq_nibble NibbleE Nibble8 = false
-  | op_eq_nibble NibbleF Nibble8 = false
-  | op_eq_nibble NibbleA Nibble9 = false
-  | op_eq_nibble NibbleB Nibble9 = false
-  | op_eq_nibble NibbleC Nibble9 = false
-  | op_eq_nibble NibbleD Nibble9 = false
-  | op_eq_nibble NibbleE Nibble9 = false
-  | op_eq_nibble NibbleF Nibble9 = false
-  | op_eq_nibble NibbleB NibbleA = false
-  | op_eq_nibble NibbleC NibbleA = false
-  | op_eq_nibble NibbleD NibbleA = false
-  | op_eq_nibble NibbleE NibbleA = false
-  | op_eq_nibble NibbleF NibbleA = false
-  | op_eq_nibble NibbleC NibbleB = false
-  | op_eq_nibble NibbleD NibbleB = false
-  | op_eq_nibble NibbleE NibbleB = false
-  | op_eq_nibble NibbleF NibbleB = false
-  | op_eq_nibble NibbleD NibbleC = false
-  | op_eq_nibble NibbleE NibbleC = false
-  | op_eq_nibble NibbleF NibbleC = false
-  | op_eq_nibble NibbleE NibbleD = false
-  | op_eq_nibble NibbleF NibbleD = false
-  | op_eq_nibble NibbleF NibbleE = false;
+fun eq_nibble Nibble0 Nibble0 = true
+  | eq_nibble Nibble1 Nibble1 = true
+  | eq_nibble Nibble2 Nibble2 = true
+  | eq_nibble Nibble3 Nibble3 = true
+  | eq_nibble Nibble4 Nibble4 = true
+  | eq_nibble Nibble5 Nibble5 = true
+  | eq_nibble Nibble6 Nibble6 = true
+  | eq_nibble Nibble7 Nibble7 = true
+  | eq_nibble Nibble8 Nibble8 = true
+  | eq_nibble Nibble9 Nibble9 = true
+  | eq_nibble NibbleA NibbleA = true
+  | eq_nibble NibbleB NibbleB = true
+  | eq_nibble NibbleC NibbleC = true
+  | eq_nibble NibbleD NibbleD = true
+  | eq_nibble NibbleE NibbleE = true
+  | eq_nibble NibbleF NibbleF = true
+  | eq_nibble Nibble0 Nibble1 = false
+  | eq_nibble Nibble0 Nibble2 = false
+  | eq_nibble Nibble0 Nibble3 = false
+  | eq_nibble Nibble0 Nibble4 = false
+  | eq_nibble Nibble0 Nibble5 = false
+  | eq_nibble Nibble0 Nibble6 = false
+  | eq_nibble Nibble0 Nibble7 = false
+  | eq_nibble Nibble0 Nibble8 = false
+  | eq_nibble Nibble0 Nibble9 = false
+  | eq_nibble Nibble0 NibbleA = false
+  | eq_nibble Nibble0 NibbleB = false
+  | eq_nibble Nibble0 NibbleC = false
+  | eq_nibble Nibble0 NibbleD = false
+  | eq_nibble Nibble0 NibbleE = false
+  | eq_nibble Nibble0 NibbleF = false
+  | eq_nibble Nibble1 Nibble2 = false
+  | eq_nibble Nibble1 Nibble3 = false
+  | eq_nibble Nibble1 Nibble4 = false
+  | eq_nibble Nibble1 Nibble5 = false
+  | eq_nibble Nibble1 Nibble6 = false
+  | eq_nibble Nibble1 Nibble7 = false
+  | eq_nibble Nibble1 Nibble8 = false
+  | eq_nibble Nibble1 Nibble9 = false
+  | eq_nibble Nibble1 NibbleA = false
+  | eq_nibble Nibble1 NibbleB = false
+  | eq_nibble Nibble1 NibbleC = false
+  | eq_nibble Nibble1 NibbleD = false
+  | eq_nibble Nibble1 NibbleE = false
+  | eq_nibble Nibble1 NibbleF = false
+  | eq_nibble Nibble2 Nibble3 = false
+  | eq_nibble Nibble2 Nibble4 = false
+  | eq_nibble Nibble2 Nibble5 = false
+  | eq_nibble Nibble2 Nibble6 = false
+  | eq_nibble Nibble2 Nibble7 = false
+  | eq_nibble Nibble2 Nibble8 = false
+  | eq_nibble Nibble2 Nibble9 = false
+  | eq_nibble Nibble2 NibbleA = false
+  | eq_nibble Nibble2 NibbleB = false
+  | eq_nibble Nibble2 NibbleC = false
+  | eq_nibble Nibble2 NibbleD = false
+  | eq_nibble Nibble2 NibbleE = false
+  | eq_nibble Nibble2 NibbleF = false
+  | eq_nibble Nibble3 Nibble4 = false
+  | eq_nibble Nibble3 Nibble5 = false
+  | eq_nibble Nibble3 Nibble6 = false
+  | eq_nibble Nibble3 Nibble7 = false
+  | eq_nibble Nibble3 Nibble8 = false
+  | eq_nibble Nibble3 Nibble9 = false
+  | eq_nibble Nibble3 NibbleA = false
+  | eq_nibble Nibble3 NibbleB = false
+  | eq_nibble Nibble3 NibbleC = false
+  | eq_nibble Nibble3 NibbleD = false
+  | eq_nibble Nibble3 NibbleE = false
+  | eq_nibble Nibble3 NibbleF = false
+  | eq_nibble Nibble4 Nibble5 = false
+  | eq_nibble Nibble4 Nibble6 = false
+  | eq_nibble Nibble4 Nibble7 = false
+  | eq_nibble Nibble4 Nibble8 = false
+  | eq_nibble Nibble4 Nibble9 = false
+  | eq_nibble Nibble4 NibbleA = false
+  | eq_nibble Nibble4 NibbleB = false
+  | eq_nibble Nibble4 NibbleC = false
+  | eq_nibble Nibble4 NibbleD = false
+  | eq_nibble Nibble4 NibbleE = false
+  | eq_nibble Nibble4 NibbleF = false
+  | eq_nibble Nibble5 Nibble6 = false
+  | eq_nibble Nibble5 Nibble7 = false
+  | eq_nibble Nibble5 Nibble8 = false
+  | eq_nibble Nibble5 Nibble9 = false
+  | eq_nibble Nibble5 NibbleA = false
+  | eq_nibble Nibble5 NibbleB = false
+  | eq_nibble Nibble5 NibbleC = false
+  | eq_nibble Nibble5 NibbleD = false
+  | eq_nibble Nibble5 NibbleE = false
+  | eq_nibble Nibble5 NibbleF = false
+  | eq_nibble Nibble6 Nibble7 = false
+  | eq_nibble Nibble6 Nibble8 = false
+  | eq_nibble Nibble6 Nibble9 = false
+  | eq_nibble Nibble6 NibbleA = false
+  | eq_nibble Nibble6 NibbleB = false
+  | eq_nibble Nibble6 NibbleC = false
+  | eq_nibble Nibble6 NibbleD = false
+  | eq_nibble Nibble6 NibbleE = false
+  | eq_nibble Nibble6 NibbleF = false
+  | eq_nibble Nibble7 Nibble8 = false
+  | eq_nibble Nibble7 Nibble9 = false
+  | eq_nibble Nibble7 NibbleA = false
+  | eq_nibble Nibble7 NibbleB = false
+  | eq_nibble Nibble7 NibbleC = false
+  | eq_nibble Nibble7 NibbleD = false
+  | eq_nibble Nibble7 NibbleE = false
+  | eq_nibble Nibble7 NibbleF = false
+  | eq_nibble Nibble8 Nibble9 = false
+  | eq_nibble Nibble8 NibbleA = false
+  | eq_nibble Nibble8 NibbleB = false
+  | eq_nibble Nibble8 NibbleC = false
+  | eq_nibble Nibble8 NibbleD = false
+  | eq_nibble Nibble8 NibbleE = false
+  | eq_nibble Nibble8 NibbleF = false
+  | eq_nibble Nibble9 NibbleA = false
+  | eq_nibble Nibble9 NibbleB = false
+  | eq_nibble Nibble9 NibbleC = false
+  | eq_nibble Nibble9 NibbleD = false
+  | eq_nibble Nibble9 NibbleE = false
+  | eq_nibble Nibble9 NibbleF = false
+  | eq_nibble NibbleA NibbleB = false
+  | eq_nibble NibbleA NibbleC = false
+  | eq_nibble NibbleA NibbleD = false
+  | eq_nibble NibbleA NibbleE = false
+  | eq_nibble NibbleA NibbleF = false
+  | eq_nibble NibbleB NibbleC = false
+  | eq_nibble NibbleB NibbleD = false
+  | eq_nibble NibbleB NibbleE = false
+  | eq_nibble NibbleB NibbleF = false
+  | eq_nibble NibbleC NibbleD = false
+  | eq_nibble NibbleC NibbleE = false
+  | eq_nibble NibbleC NibbleF = false
+  | eq_nibble NibbleD NibbleE = false
+  | eq_nibble NibbleD NibbleF = false
+  | eq_nibble NibbleE NibbleF = false
+  | eq_nibble Nibble1 Nibble0 = false
+  | eq_nibble Nibble2 Nibble0 = false
+  | eq_nibble Nibble3 Nibble0 = false
+  | eq_nibble Nibble4 Nibble0 = false
+  | eq_nibble Nibble5 Nibble0 = false
+  | eq_nibble Nibble6 Nibble0 = false
+  | eq_nibble Nibble7 Nibble0 = false
+  | eq_nibble Nibble8 Nibble0 = false
+  | eq_nibble Nibble9 Nibble0 = false
+  | eq_nibble NibbleA Nibble0 = false
+  | eq_nibble NibbleB Nibble0 = false
+  | eq_nibble NibbleC Nibble0 = false
+  | eq_nibble NibbleD Nibble0 = false
+  | eq_nibble NibbleE Nibble0 = false
+  | eq_nibble NibbleF Nibble0 = false
+  | eq_nibble Nibble2 Nibble1 = false
+  | eq_nibble Nibble3 Nibble1 = false
+  | eq_nibble Nibble4 Nibble1 = false
+  | eq_nibble Nibble5 Nibble1 = false
+  | eq_nibble Nibble6 Nibble1 = false
+  | eq_nibble Nibble7 Nibble1 = false
+  | eq_nibble Nibble8 Nibble1 = false
+  | eq_nibble Nibble9 Nibble1 = false
+  | eq_nibble NibbleA Nibble1 = false
+  | eq_nibble NibbleB Nibble1 = false
+  | eq_nibble NibbleC Nibble1 = false
+  | eq_nibble NibbleD Nibble1 = false
+  | eq_nibble NibbleE Nibble1 = false
+  | eq_nibble NibbleF Nibble1 = false
+  | eq_nibble Nibble3 Nibble2 = false
+  | eq_nibble Nibble4 Nibble2 = false
+  | eq_nibble Nibble5 Nibble2 = false
+  | eq_nibble Nibble6 Nibble2 = false
+  | eq_nibble Nibble7 Nibble2 = false
+  | eq_nibble Nibble8 Nibble2 = false
+  | eq_nibble Nibble9 Nibble2 = false
+  | eq_nibble NibbleA Nibble2 = false
+  | eq_nibble NibbleB Nibble2 = false
+  | eq_nibble NibbleC Nibble2 = false
+  | eq_nibble NibbleD Nibble2 = false
+  | eq_nibble NibbleE Nibble2 = false
+  | eq_nibble NibbleF Nibble2 = false
+  | eq_nibble Nibble4 Nibble3 = false
+  | eq_nibble Nibble5 Nibble3 = false
+  | eq_nibble Nibble6 Nibble3 = false
+  | eq_nibble Nibble7 Nibble3 = false
+  | eq_nibble Nibble8 Nibble3 = false
+  | eq_nibble Nibble9 Nibble3 = false
+  | eq_nibble NibbleA Nibble3 = false
+  | eq_nibble NibbleB Nibble3 = false
+  | eq_nibble NibbleC Nibble3 = false
+  | eq_nibble NibbleD Nibble3 = false
+  | eq_nibble NibbleE Nibble3 = false
+  | eq_nibble NibbleF Nibble3 = false
+  | eq_nibble Nibble5 Nibble4 = false
+  | eq_nibble Nibble6 Nibble4 = false
+  | eq_nibble Nibble7 Nibble4 = false
+  | eq_nibble Nibble8 Nibble4 = false
+  | eq_nibble Nibble9 Nibble4 = false
+  | eq_nibble NibbleA Nibble4 = false
+  | eq_nibble NibbleB Nibble4 = false
+  | eq_nibble NibbleC Nibble4 = false
+  | eq_nibble NibbleD Nibble4 = false
+  | eq_nibble NibbleE Nibble4 = false
+  | eq_nibble NibbleF Nibble4 = false
+  | eq_nibble Nibble6 Nibble5 = false
+  | eq_nibble Nibble7 Nibble5 = false
+  | eq_nibble Nibble8 Nibble5 = false
+  | eq_nibble Nibble9 Nibble5 = false
+  | eq_nibble NibbleA Nibble5 = false
+  | eq_nibble NibbleB Nibble5 = false
+  | eq_nibble NibbleC Nibble5 = false
+  | eq_nibble NibbleD Nibble5 = false
+  | eq_nibble NibbleE Nibble5 = false
+  | eq_nibble NibbleF Nibble5 = false
+  | eq_nibble Nibble7 Nibble6 = false
+  | eq_nibble Nibble8 Nibble6 = false
+  | eq_nibble Nibble9 Nibble6 = false
+  | eq_nibble NibbleA Nibble6 = false
+  | eq_nibble NibbleB Nibble6 = false
+  | eq_nibble NibbleC Nibble6 = false
+  | eq_nibble NibbleD Nibble6 = false
+  | eq_nibble NibbleE Nibble6 = false
+  | eq_nibble NibbleF Nibble6 = false
+  | eq_nibble Nibble8 Nibble7 = false
+  | eq_nibble Nibble9 Nibble7 = false
+  | eq_nibble NibbleA Nibble7 = false
+  | eq_nibble NibbleB Nibble7 = false
+  | eq_nibble NibbleC Nibble7 = false
+  | eq_nibble NibbleD Nibble7 = false
+  | eq_nibble NibbleE Nibble7 = false
+  | eq_nibble NibbleF Nibble7 = false
+  | eq_nibble Nibble9 Nibble8 = false
+  | eq_nibble NibbleA Nibble8 = false
+  | eq_nibble NibbleB Nibble8 = false
+  | eq_nibble NibbleC Nibble8 = false
+  | eq_nibble NibbleD Nibble8 = false
+  | eq_nibble NibbleE Nibble8 = false
+  | eq_nibble NibbleF Nibble8 = false
+  | eq_nibble NibbleA Nibble9 = false
+  | eq_nibble NibbleB Nibble9 = false
+  | eq_nibble NibbleC Nibble9 = false
+  | eq_nibble NibbleD Nibble9 = false
+  | eq_nibble NibbleE Nibble9 = false
+  | eq_nibble NibbleF Nibble9 = false
+  | eq_nibble NibbleB NibbleA = false
+  | eq_nibble NibbleC NibbleA = false
+  | eq_nibble NibbleD NibbleA = false
+  | eq_nibble NibbleE NibbleA = false
+  | eq_nibble NibbleF NibbleA = false
+  | eq_nibble NibbleC NibbleB = false
+  | eq_nibble NibbleD NibbleB = false
+  | eq_nibble NibbleE NibbleB = false
+  | eq_nibble NibbleF NibbleB = false
+  | eq_nibble NibbleD NibbleC = false
+  | eq_nibble NibbleE NibbleC = false
+  | eq_nibble NibbleF NibbleC = false
+  | eq_nibble NibbleE NibbleD = false
+  | eq_nibble NibbleF NibbleD = false
+  | eq_nibble NibbleF NibbleE = false;
 
-fun op_eq_char (Char (nibble1, nibble2)) (Char (nibble1', nibble2')) =
-  op_eq_nibble nibble1 nibble1' andalso op_eq_nibble nibble2 nibble2';
+fun eq_char (Char (nibble1, nibble2)) (Char (nibble1', nibble2')) =
+  eq_nibble nibble1 nibble1' andalso eq_nibble nibble2 nibble2';
+
+val eq_chara = {eq = eq_char} : char Code_Generator.eq;
 
-val eq_char = {op_eq = op_eq_char} : char Code_Generator.eq;
+fun eq_list A_ [] [] = true
+  | eq_list A_ (a :: lista) (a' :: list') =
+    Code_Generator.eq A_ a a' andalso eq_list A_ lista list'
+  | eq_list A_ [] (a :: b) = false
+  | eq_list A_ (a :: b) [] = false;
 
 fun list_all p (x :: xs) = p x andalso list_all p xs
   | list_all p [] = true;
@@ -313,15 +319,9 @@
   | list_all2 p xs [] = null xs
   | list_all2 p [] ys = null ys
   | list_all2 p xs ys =
-    Nat.op_eq_nat (size_list xs) (size_list ys) andalso
+    Nat.eq_nat (size_list xs) (size_list ys) andalso
       list_all (fn a as (aa, b) => p aa b) (zip xs ys);
 
-fun op_eq_list A_ [] [] = true
-  | op_eq_list A_ (a :: lista) (a' :: list') =
-    Code_Generator.op_eq A_ a a' andalso op_eq_list A_ lista list'
-  | op_eq_list A_ [] (a :: b) = false
-  | op_eq_list A_ (a :: b) [] = false;
-
 end; (*struct List*)
 
 structure Codegen = 
@@ -329,9 +329,9 @@
 
 datatype monotype = Mono of List.char list * monotype list;
 
-fun op_eq_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =
-  List.op_eq_list List.eq_char tyco1 tyco2 andalso
-    List.list_all2 op_eq_monotype typargs1 typargs2;
+fun eq_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =
+  List.eq_list List.eq_chara tyco1 tyco2 andalso
+    List.list_all2 eq_monotype typargs1 typargs2;
 
 end; (*struct Codegen*)
 

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML	Fri May 25 21:08:45 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML	Fri May 25 21:08:46 2007 +0200
@@ -4,8 +4,8 @@
 structure Code_Generator = 
 struct
 
-type 'a eq = {op_eq : 'a -> 'a -> bool};
-fun op_eq (A_:'a eq) = #op_eq A_;
+type 'a eq = {eq : 'a -> 'a -> bool};
+fun eq (A_:'a eq) = #eq A_;
 
 end; (*struct Code_Generator*)
 
@@ -16,7 +16,7 @@
   | foldr f [] a = a;
 
 fun memberl A_ x (y :: ys) =
-  Code_Generator.op_eq A_ x y orelse memberl A_ x ys
+  Code_Generator.eq A_ x y orelse memberl A_ x ys
   | memberl A_ x [] = false;
 
 end; (*struct List*)
@@ -26,15 +26,15 @@
 
 datatype 'a set = Set of 'a list;
 
-fun opa A_ x (Set xs) = List.memberl A_ x xs;
-
 val empty : 'a set = Set [];
 
 fun insert x (Set xs) = Set (x :: xs);
 
-fun op_Un xs (Set ys) = List.foldr insert ys xs;
+fun uniona xs (Set ys) = List.foldr insert ys xs;
 
-fun union (Set xs) = List.foldr op_Un xs empty;
+fun union (Set xs) = List.foldr uniona xs empty;
+
+fun member A_ x (Set xs) = List.memberl A_ x xs;
 
 end; (*struct Set*)
 

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML	Fri May 25 21:08:45 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML	Fri May 25 21:08:46 2007 +0200
@@ -13,8 +13,8 @@
 structure Code_Generator = 
 struct
 
-type 'a eq = {op_eq : 'a -> 'a -> bool};
-fun op_eq (A_:'a eq) = #op_eq A_;
+type 'a eq = {eq : 'a -> 'a -> bool};
+fun eq (A_:'a eq) = #eq A_;
 
 end; (*struct Code_Generator*)
 
@@ -23,12 +23,12 @@
 
 datatype nat = Zero_nat | Suc of nat;
 
-fun op_eq_nat Zero_nat (Suc m) = false
-  | op_eq_nat (Suc n) Zero_nat = false
-  | op_eq_nat (Suc n) (Suc m) = op_eq_nat n m
-  | op_eq_nat Zero_nat Zero_nat = true;
+fun eq_nat Zero_nat (Suc m) = false
+  | eq_nat (Suc n) Zero_nat = false
+  | eq_nat (Suc n) (Suc m) = eq_nat n m
+  | eq_nat Zero_nat Zero_nat = true;
 
-val eq_nat = {op_eq = op_eq_nat} : nat Code_Generator.eq;
+val eq_nata = {eq = eq_nat} : nat Code_Generator.eq;
 
 fun less_nat n (Suc m) = less_eq_nat n m
   | less_nat n Zero_nat = false
@@ -62,13 +62,13 @@
     then Branch (update (C1_, C2_) (it, entry) t1, key, t2)
     else Branch (t1, key, update (C1_, C2_) (it, entry) t2))
   | update (C1_, C2_) (it, entry) (Leaf (key, vala)) =
-    (if Code_Generator.op_eq C1_ it key then Leaf (key, entry)
+    (if Code_Generator.eq C1_ it key then Leaf (key, entry)
       else (if Orderings.less_eq C2_ it key
              then Branch (Leaf (it, entry), it, Leaf (key, vala))
              else Branch (Leaf (key, vala), it, Leaf (it, entry))));
 
 fun example n =
-  update (Nat.eq_nat, Nat.ord_nat)
+  update (Nat.eq_nata, Nat.ord_nat)
     (n, [List.Char (List.Nibble6, List.Nibble2),
           List.Char (List.Nibble6, List.Nibble1),
           List.Char (List.Nibble7, List.Nibble2)])