doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML
changeset 22386 4ebe883b02ff
parent 22188 a63889770d57
child 22751 1bfd75c1f232
equal deleted inserted replaced
22385:cc2be3315e72 22386:4ebe883b02ff
     2 struct
     2 struct
     3 
     3 
     4 structure Code_Generator = 
     4 structure Code_Generator = 
     5 struct
     5 struct
     6 
     6 
     7 type 'a eq = {Code_Generator__op_eq : 'a -> 'a -> bool};
     7 type 'a eq = {op_eq : 'a -> 'a -> bool};
     8 fun op_eq (A_:'a eq) = #Code_Generator__op_eq A_;
     8 fun op_eq (A_:'a eq) = #op_eq A_;
     9 
     9 
    10 end; (*struct Code_Generator*)
    10 end; (*struct Code_Generator*)
    11 
    11 
    12 structure List = 
    12 structure List = 
    13 struct
    13 struct