# HG changeset patch
# User haftmann
# Date 1272466578 -7200
# Node ID 70096cbdd4e002b3645c810c247903fa14812755
# Parent  3e677ca1e564fbc162938b6323f6b53fb5891971
avoid code_datatype antiquotation

diff -r 3e677ca1e564 -r 70096cbdd4e0 src/HOL/Lazy_Sequence.thy
--- a/src/HOL/Lazy_Sequence.thy	Wed Apr 28 15:42:10 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Wed Apr 28 16:56:18 2010 +0200
@@ -123,6 +123,13 @@
 
 subsection {* Code setup *}
 
+code_reflect
+  datatypes lazy_sequence = Lazy_Sequence
+  functions "Lazy_Sequence.map" yield
+  module_name Lazy_Sequence
+
+(* FIXME formulate yieldn in the logic with type code_numeral *)
+
 ML {*
 signature LAZY_SEQUENCE =
 sig
@@ -135,9 +142,9 @@
 structure Lazy_Sequence : LAZY_SEQUENCE =
 struct
 
-@{code_datatype lazy_sequence = Lazy_Sequence}
+open Lazy_Sequence;
 
-val yield = @{code yield}
+fun map f = mapa f;
 
 fun anamorph f k x = (if k = 0 then ([], x)
   else case f x
@@ -148,17 +155,9 @@
 
 fun yieldn S = anamorph yield S;
 
-val map = @{code map}
-
 end;
 *}
 
-code_reserved Eval Lazy_Sequence
-
-code_type lazy_sequence (Eval "_/ Lazy'_Sequence.lazy'_sequence")
-
-code_const Lazy_Sequence (Eval "Lazy'_Sequence.Lazy'_Sequence")
-
 section {* With Hit Bound Value *}
 text {* assuming in negative context *}
 
diff -r 3e677ca1e564 -r 70096cbdd4e0 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Wed Apr 28 15:42:10 2010 +0200
+++ b/src/HOL/Predicate.thy	Wed Apr 28 16:56:18 2010 +0200
@@ -880,6 +880,11 @@
 
 code_abort not_unique
 
+code_reflect
+  datatypes pred = Seq and seq = Empty | Insert | Join
+  functions map
+  module_name Predicate
+
 ML {*
 signature PREDICATE =
 sig
@@ -893,15 +898,17 @@
 structure Predicate : PREDICATE =
 struct
 
-@{code_datatype pred = Seq};
-@{code_datatype seq = Empty | Insert | Join};
+datatype pred = datatype Predicate.pred
+datatype seq = datatype Predicate.seq
+
+fun map f = Predicate.map f;
 
-fun yield (@{code Seq} f) = next (f ())
-and next @{code Empty} = NONE
-  | next (@{code Insert} (x, P)) = SOME (x, P)
-  | next (@{code Join} (P, xq)) = (case yield P
+fun yield (Seq f) = next (f ())
+and next Empty = NONE
+  | next (Insert (x, P)) = SOME (x, P)
+  | next (Join (P, xq)) = (case yield P
      of NONE => next xq
-      | SOME (x, Q) => SOME (x, @{code Seq} (fn _ => @{code Join} (Q, xq))));
+      | SOME (x, Q) => SOME (x, Seq (fn _ => Join (Q, xq))));
 
 fun anamorph f k x = (if k = 0 then ([], x)
   else case f x
@@ -912,19 +919,9 @@
 
 fun yieldn P = anamorph yield P;
 
-fun map f = @{code map} f;
-
 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