doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML

Reintroduce set_interpreter for Collect and op :.
I removed them by accident when removing old code that dealt with the "set" type.
Incidentally, there is still some broken "set" code in Refute that should be fixed (see TODO in refute.ML).

structure Nat = 
struct

datatype nat = Suc of nat | Zero_nat;

end; (*struct Nat*)

structure Codegen = 
struct

type 'a null = {null : 'a};
fun null (A_:'a null) = #null A_;

fun head A_ (x :: xs) = x
  | head A_ [] = null A_;

val null_option : 'a option = NONE;

fun null_optiona () = {null = null_option} : ('a option) null;

val dummy : Nat.nat option =
  head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];

end; (*struct Codegen*)