The generated code is as follows. Function re_lit comes out exactly
as expected, except for its first argument. It was "supposed" to be
the function that checks if the list in its second argument starts
with the item in its first argument.

**********
structure re_lit : sig
type 'a eq
val eq : 'a eq -> 'a -> 'a -> bool
val eqa : 'a eq -> 'a -> 'a -> bool
val re_lit : 'a eq -> 'a -> 'a list -> (('a list * 'a list) list) option
end = struct

type 'a eq = {eq : 'a -> 'a -> bool};
val eq = #eq : 'a eq -> 'a -> 'a -> bool;

fun eqa A_ a b = eq A_ a b;

fun re_lit A_ x sigma =
(if eqa A_ (hd sigma) x then SOME [([x], tl sigma)] else NONE);

end; (*struct re_lit*)
*********

I do not understand the "type 'a eq" construction and how to use it.
Any references (or hints on how to google this) or of course
explanations would be greatly appreciated.

Best,
Bart