renamed type Lazy.T to lazy;
authorwenzelm
Thu Dec 04 23:00:21 2008 +0100 (2008-12-04)
changeset 28971300ec36a19af
parent 28945 da79ac67794b
child 28972 cb8a2c3e188f
renamed type Lazy.T to lazy;
src/HOL/Import/lazy_seq.ML
src/Pure/General/lazy.ML
src/Pure/Isar/code.ML
src/Pure/proofterm.ML
src/Tools/code/code_ml.ML
     1.1 --- a/src/HOL/Import/lazy_seq.ML	Tue Dec 02 14:29:12 2008 +0100
     1.2 +++ b/src/HOL/Import/lazy_seq.ML	Thu Dec 04 23:00:21 2008 +0100
     1.3 @@ -80,7 +80,7 @@
     1.4  structure LazySeq :> LAZY_SEQ =
     1.5  struct
     1.6  
     1.7 -datatype 'a seq = Seq of ('a * 'a seq) option Lazy.T
     1.8 +datatype 'a seq = Seq of ('a * 'a seq) option lazy
     1.9  
    1.10  exception Empty
    1.11  
     2.1 --- a/src/Pure/General/lazy.ML	Tue Dec 02 14:29:12 2008 +0100
     2.2 +++ b/src/Pure/General/lazy.ML	Thu Dec 04 23:00:21 2008 +0100
     2.3 @@ -8,13 +8,13 @@
     2.4  
     2.5  signature LAZY =
     2.6  sig
     2.7 -  type 'a T
     2.8 -  val same: 'a T * 'a T -> bool
     2.9 -  val lazy: (unit -> 'a) -> 'a T
    2.10 -  val value: 'a -> 'a T
    2.11 -  val peek: 'a T -> 'a Exn.result option
    2.12 -  val force: 'a T -> 'a
    2.13 -  val map_force: ('a -> 'a) -> 'a T -> 'a T
    2.14 +  type 'a lazy
    2.15 +  val same: 'a lazy * 'a lazy -> bool
    2.16 +  val lazy: (unit -> 'a) -> 'a lazy
    2.17 +  val value: 'a -> 'a lazy
    2.18 +  val peek: 'a lazy -> 'a Exn.result option
    2.19 +  val force: 'a lazy -> 'a
    2.20 +  val map_force: ('a -> 'a) -> 'a lazy -> 'a lazy
    2.21  end
    2.22  
    2.23  structure Lazy :> LAZY =
    2.24 @@ -22,13 +22,13 @@
    2.25  
    2.26  (* datatype *)
    2.27  
    2.28 -datatype 'a lazy =
    2.29 +datatype 'a T =
    2.30    Lazy of unit -> 'a |
    2.31    Result of 'a Exn.result;
    2.32  
    2.33 -type 'a T = 'a lazy ref;
    2.34 +type 'a lazy = 'a T ref;
    2.35  
    2.36 -fun same (r1: 'a T, r2) = r1 = r2;
    2.37 +fun same (r1: 'a lazy, r2) = r1 = r2;
    2.38  
    2.39  fun lazy e = ref (Lazy e);
    2.40  fun value x = ref (Result (Exn.Result x));
    2.41 @@ -58,3 +58,6 @@
    2.42  fun map_force f = value o f o force;
    2.43  
    2.44  end;
    2.45 +
    2.46 +type 'a lazy = 'a Lazy.lazy;
    2.47 +
     3.1 --- a/src/Pure/Isar/code.ML	Tue Dec 02 14:29:12 2008 +0100
     3.2 +++ b/src/Pure/Isar/code.ML	Thu Dec 04 23:00:21 2008 +0100
     3.3 @@ -15,7 +15,7 @@
     3.4    val add_default_eqn_attrib: Attrib.src
     3.5    val del_eqn: thm -> theory -> theory
     3.6    val del_eqns: string -> theory -> theory
     3.7 -  val add_eqnl: string * (thm * bool) list Lazy.T -> theory -> theory
     3.8 +  val add_eqnl: string * (thm * bool) list lazy -> theory -> theory
     3.9    val map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
    3.10    val map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
    3.11    val add_inline: thm -> theory -> theory
    3.12 @@ -114,7 +114,7 @@
    3.13  
    3.14  (* defining equations *)
    3.15  
    3.16 -type eqns = bool * (thm * bool) list Lazy.T;
    3.17 +type eqns = bool * (thm * bool) list lazy;
    3.18    (*default flag, theorems with linear flag (perhaps lazy)*)
    3.19  
    3.20  fun pretty_lthms ctxt r = case Lazy.peek r
     4.1 --- a/src/Pure/proofterm.ML	Tue Dec 02 14:29:12 2008 +0100
     4.2 +++ b/src/Pure/proofterm.ML	Thu Dec 04 23:00:21 2008 +0100
     4.3 @@ -22,10 +22,10 @@
     4.4     | PAxm of string * term * typ list option
     4.5     | Oracle of string * term * typ list option
     4.6     | Promise of serial * term * typ list
     4.7 -   | PThm of serial * ((string * term * typ list option) * proof_body Lazy.T)
     4.8 +   | PThm of serial * ((string * term * typ list option) * proof_body lazy)
     4.9    and proof_body = PBody of
    4.10      {oracles: (string * term) OrdList.T,
    4.11 -     thms: (serial * (string * term * proof_body Lazy.T)) OrdList.T,
    4.12 +     thms: (serial * (string * term * proof_body lazy)) OrdList.T,
    4.13       proof: proof}
    4.14  
    4.15    val %> : proof * term -> proof
    4.16 @@ -36,10 +36,10 @@
    4.17    include BASIC_PROOFTERM
    4.18  
    4.19    type oracle = string * term
    4.20 -  type pthm = serial * (string * term * proof_body Lazy.T)
    4.21 -  val force_body: proof_body Lazy.T ->
    4.22 +  type pthm = serial * (string * term * proof_body lazy)
    4.23 +  val force_body: proof_body lazy ->
    4.24      {oracles: oracle OrdList.T, thms: pthm OrdList.T, proof: proof}
    4.25 -  val force_proof: proof_body Lazy.T -> proof
    4.26 +  val force_proof: proof_body lazy -> proof
    4.27    val proof_of: proof_body -> proof
    4.28    val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
    4.29    val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
    4.30 @@ -111,7 +111,7 @@
    4.31    val promise_proof: theory -> serial -> term -> proof
    4.32    val fulfill_proof: theory -> (serial * proof) list -> proof_body -> proof_body
    4.33    val thm_proof: theory -> string -> term list -> term ->
    4.34 -    (serial * proof) list Lazy.T -> proof_body -> pthm * proof
    4.35 +    (serial * proof) list lazy -> proof_body -> pthm * proof
    4.36    val get_name: term list -> term -> proof -> string
    4.37  
    4.38    (** rewriting on proof terms **)
    4.39 @@ -143,14 +143,14 @@
    4.40   | PAxm of string * term * typ list option
    4.41   | Oracle of string * term * typ list option
    4.42   | Promise of serial * term * typ list
    4.43 - | PThm of serial * ((string * term * typ list option) * proof_body Lazy.T)
    4.44 + | PThm of serial * ((string * term * typ list option) * proof_body lazy)
    4.45  and proof_body = PBody of
    4.46    {oracles: (string * term) OrdList.T,
    4.47 -   thms: (serial * (string * term * proof_body Lazy.T)) OrdList.T,
    4.48 +   thms: (serial * (string * term * proof_body lazy)) OrdList.T,
    4.49     proof: proof};
    4.50  
    4.51  type oracle = string * term;
    4.52 -type pthm = serial * (string * term * proof_body Lazy.T);
    4.53 +type pthm = serial * (string * term * proof_body lazy);
    4.54  
    4.55  val force_body = Lazy.force #> (fn PBody args => args);
    4.56  val force_proof = #proof o force_body;
     5.1 --- a/src/Tools/code/code_ml.ML	Tue Dec 02 14:29:12 2008 +0100
     5.2 +++ b/src/Tools/code/code_ml.ML	Thu Dec 04 23:00:21 2008 +0100
     5.3 @@ -912,7 +912,7 @@
     5.4  
     5.5  structure CodeAntiqData = ProofDataFun
     5.6  (
     5.7 -  type T = string list * (bool * (string * (string * (string * string) list) Lazy.T));
     5.8 +  type T = string list * (bool * (string * (string * (string * string) list) lazy));
     5.9    fun init _ = ([], (true, ("", Lazy.value ("", []))));
    5.10  );
    5.11