src/Pure/General/susp.ML

type proof: theory_ref instead of theory (make proof contexts independent entities);
added transfer_proof;

(*  Title:      Pure/General/susp.ML
    ID:         $Id$
    Author:     Sebastian Skalberg, TU Muenchen

Delayed evaluation.
*)

signature SUSP =
sig

type 'a susp

val force : 'a susp -> 'a
val delay : (unit -> 'a) -> 'a susp
val value : 'a -> 'a susp

end

structure Susp :> SUSP =
struct

datatype 'a suspVal
  = Value of 'a
  | Delay of unit -> 'a

type 'a susp = 'a suspVal ref

fun force (ref (Value v)) = v
  | force (r as ref (Delay f)) =
    let
	val v = f ()
    in
	r := Value v;
	v
    end

fun delay f = ref (Delay f)

fun value v = ref (Value v)

end