--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Tue Nov 21 20:58:15 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Wed Nov 22 10:20:09 2006 +0100
@@ -4,16 +4,17 @@
structure Code_Generator =
struct
-type 'a eq = {eq_ : 'a -> 'a -> bool};
-fun eq (A_:'a eq) = #eq_ A_;
+type 'a eq = {op_eq_ : 'a -> 'a -> bool};
+fun op_eq (A_:'a eq) = #op_eq_ A_;
end; (*struct Code_Generator*)
structure Product_Type =
struct
-fun eq_prod (A_:'a Code_Generator.eq) (B_:'b Code_Generator.eq) (x1, y1)
- (x2, y2) = Code_Generator.eq A_ x1 x2 andalso Code_Generator.eq B_ y1 y2;
+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;
end; (*struct Product_Type*)
@@ -36,14 +37,14 @@
val (x2a, y2a) = p2;
in
Orderings.less (#2 B_) x1a x2a orelse
- Code_Generator.eq (#1 B_) x1a x2a andalso
+ Code_Generator.op_eq (#1 B_) x1a x2a andalso
Orderings.less (#2 C_) y1a y2a
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.eq_prod (#1 B_) (#1 C_) p1 p2;
+ Product_Type.op_eq_prod (#1 B_) (#1 C_) p1 p2;
end; (*struct Codegen*)