# HG changeset patch
# User haftmann
# Date 1239974046 -7200
# Node ID 7f699568a877c8f5f825cba8f1b3f75365969353
# Parent  dd551284a3001e12ed939a5649811786b205702f
static compilation of enumeration type

diff -r dd551284a300 -r 7f699568a877 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Fri Apr 17 14:29:56 2009 +0200
+++ b/src/HOL/Predicate.thy	Fri Apr 17 15:14:06 2009 +0200
@@ -622,6 +622,31 @@
   "pred_rec f P = f (eval P)"
   by (cases P) simp
 
+export_code Seq in Eval module_name Predicate
+
+ML {*
+signature PREDICATE =
+sig
+  datatype 'a pred = Seq of (unit -> 'a seq)
+  and 'a seq = Empty | Insert of 'a * 'a pred | Join of 'a pred * 'a seq
+end;
+
+structure Predicate : PREDICATE =
+struct
+
+open Predicate;
+
+end;
+*}
+
+code_reserved Eval Predicate
+
+code_type pred and seq
+  (Eval "_/ Predicate.pred" and "_/ Predicate.seq")
+
+code_const Seq and Empty and Insert and Join
+  (Eval "Predicate.Seq" and "Predicate.Empty" and "Predicate.Insert/ (_,/ _)" and "Predicate.Join/ (_,/ _)")
+
 no_notation
   inf (infixl "\<sqinter>" 70) and
   sup (infixl "\<squnion>" 65) and