1.1 --- a/src/HOL/Lazy_Sequence.thy	Wed Apr 28 15:42:10 2010 +0200
     1.2 +++ b/src/HOL/Lazy_Sequence.thy	Wed Apr 28 16:56:18 2010 +0200
     1.3 @@ -123,6 +123,13 @@
     1.4  
     1.5  subsection {* Code setup *}
     1.6  
     1.7 +code_reflect
     1.8 +  datatypes lazy_sequence = Lazy_Sequence
     1.9 +  functions "Lazy_Sequence.map" yield
    1.10 +  module_name Lazy_Sequence
    1.11 +
    1.12 +(* FIXME formulate yieldn in the logic with type code_numeral *)
    1.13 +
    1.14  ML {*
    1.15  signature LAZY_SEQUENCE =
    1.16  sig
    1.17 @@ -135,9 +142,9 @@
    1.18  structure Lazy_Sequence : LAZY_SEQUENCE =
    1.19  struct
    1.20  
    1.21 -@{code_datatype lazy_sequence = Lazy_Sequence}
    1.22 +open Lazy_Sequence;
    1.23  
    1.24 -val yield = @{code yield}
    1.25 +fun map f = mapa f;
    1.26  
    1.27  fun anamorph f k x = (if k = 0 then ([], x)
    1.28    else case f x
    1.29 @@ -148,17 +155,9 @@
    1.30  
    1.31  fun yieldn S = anamorph yield S;
    1.32  
    1.33 -val map = @{code map}
    1.34 -
    1.35  end;
    1.36  *}
    1.37  
    1.38 -code_reserved Eval Lazy_Sequence
    1.39 -
    1.40 -code_type lazy_sequence (Eval "_/ Lazy'_Sequence.lazy'_sequence")
    1.41 -
    1.42 -code_const Lazy_Sequence (Eval "Lazy'_Sequence.Lazy'_Sequence")
    1.43 -
    1.44  section {* With Hit Bound Value *}
    1.45  text {* assuming in negative context *}
    1.46  

     2.1 --- a/src/HOL/Predicate.thy	Wed Apr 28 15:42:10 2010 +0200
     2.2 +++ b/src/HOL/Predicate.thy	Wed Apr 28 16:56:18 2010 +0200
     2.3 @@ -880,6 +880,11 @@
     2.4  
     2.5  code_abort not_unique
     2.6  
     2.7 +code_reflect
     2.8 +  datatypes pred = Seq and seq = Empty | Insert | Join
     2.9 +  functions map
    2.10 +  module_name Predicate
    2.11 +
    2.12  ML {*
    2.13  signature PREDICATE =
    2.14  sig
    2.15 @@ -893,15 +898,17 @@
    2.16  structure Predicate : PREDICATE =
    2.17  struct
    2.18  
    2.19 -@{code_datatype pred = Seq};
    2.20 -@{code_datatype seq = Empty | Insert | Join};
    2.21 +datatype pred = datatype Predicate.pred
    2.22 +datatype seq = datatype Predicate.seq
    2.23  
    2.24 -fun yield (@{code Seq} f) = next (f ())
    2.25 -and next @{code Empty} = NONE
    2.26 -  | next (@{code Insert} (x, P)) = SOME (x, P)
    2.27 -  | next (@{code Join} (P, xq)) = (case yield P
    2.28 +fun map f = Predicate.map f;
    2.29 +
    2.30 +fun yield (Seq f) = next (f ())
    2.31 +and next Empty = NONE
    2.32 +  | next (Insert (x, P)) = SOME (x, P)
    2.33 +  | next (Join (P, xq)) = (case yield P
    2.34       of NONE => next xq
    2.35 -      | SOME (x, Q) => SOME (x, @{code Seq} (fn _ => @{code Join} (Q, xq))));
    2.36 +      | SOME (x, Q) => SOME (x, Seq (fn _ => Join (Q, xq))));
    2.37  
    2.38  fun anamorph f k x = (if k = 0 then ([], x)
    2.39    else case f x
    2.40 @@ -912,19 +919,9 @@
    2.41  
    2.42  fun yieldn P = anamorph yield P;
    2.43  
    2.44 -fun map f = @{code map} f;
    2.45 -
    2.46  end;
    2.47  *}
    2.48  
    2.49 -code_reserved Eval Predicate
    2.50 -
    2.51 -code_type pred and seq
    2.52 -  (Eval "_/ Predicate.pred" and "_/ Predicate.seq")
    2.53 -
    2.54 -code_const Seq and Empty and Insert and Join
    2.55 -  (Eval "Predicate.Seq" and "Predicate.Empty" and "Predicate.Insert/ (_,/ _)" and "Predicate.Join/ (_,/ _)")
    2.56 -
    2.57  no_notation
    2.58    inf (infixl "\<sqinter>" 70) and
    2.59    sup (infixl "\<squnion>" 65) and