1.1 --- a/src/HOL/Predicate.thy	Fri Apr 17 14:29:56 2009 +0200
     1.2 +++ b/src/HOL/Predicate.thy	Fri Apr 17 15:14:06 2009 +0200
     1.3 @@ -622,6 +622,31 @@
     1.4    "pred_rec f P = f (eval P)"
     1.5    by (cases P) simp
     1.6  
     1.7 +export_code Seq in Eval module_name Predicate
     1.8 +
     1.9 +ML {*
    1.10 +signature PREDICATE =
    1.11 +sig
    1.12 +  datatype 'a pred = Seq of (unit -> 'a seq)
    1.13 +  and 'a seq = Empty | Insert of 'a * 'a pred | Join of 'a pred * 'a seq
    1.14 +end;
    1.15 +
    1.16 +structure Predicate : PREDICATE =
    1.17 +struct
    1.18 +
    1.19 +open Predicate;
    1.20 +
    1.21 +end;
    1.22 +*}
    1.23 +
    1.24 +code_reserved Eval Predicate
    1.25 +
    1.26 +code_type pred and seq
    1.27 +  (Eval "_/ Predicate.pred" and "_/ Predicate.seq")
    1.28 +
    1.29 +code_const Seq and Empty and Insert and Join
    1.30 +  (Eval "Predicate.Seq" and "Predicate.Empty" and "Predicate.Insert/ (_,/ _)" and "Predicate.Join/ (_,/ _)")
    1.31 +
    1.32  no_notation
    1.33    inf (infixl "\<sqinter>" 70) and
    1.34    sup (infixl "\<squnion>" 65) and