# HG changeset patch
# User wenzelm
# Date 1228428021 -3600
# Node ID 300ec36a19af3243d952fe093e5dfcd56eb1b9ac
# Parent  da79ac67794b7d57893736da032d3645d9bf1924
renamed type Lazy.T to lazy;

diff -r da79ac67794b -r 300ec36a19af src/HOL/Import/lazy_seq.ML
--- a/src/HOL/Import/lazy_seq.ML	Tue Dec 02 14:29:12 2008 +0100
+++ b/src/HOL/Import/lazy_seq.ML	Thu Dec 04 23:00:21 2008 +0100
@@ -80,7 +80,7 @@
 structure LazySeq :> LAZY_SEQ =
 struct
 
-datatype 'a seq = Seq of ('a * 'a seq) option Lazy.T
+datatype 'a seq = Seq of ('a * 'a seq) option lazy
 
 exception Empty
 
diff -r da79ac67794b -r 300ec36a19af src/Pure/General/lazy.ML
--- a/src/Pure/General/lazy.ML	Tue Dec 02 14:29:12 2008 +0100
+++ b/src/Pure/General/lazy.ML	Thu Dec 04 23:00:21 2008 +0100
@@ -8,13 +8,13 @@
 
 signature LAZY =
 sig
-  type 'a T
-  val same: 'a T * 'a T -> bool
-  val lazy: (unit -> 'a) -> 'a T
-  val value: 'a -> 'a T
-  val peek: 'a T -> 'a Exn.result option
-  val force: 'a T -> 'a
-  val map_force: ('a -> 'a) -> 'a T -> 'a T
+  type 'a lazy
+  val same: 'a lazy * 'a lazy -> bool
+  val lazy: (unit -> 'a) -> 'a lazy
+  val value: 'a -> 'a lazy
+  val peek: 'a lazy -> 'a Exn.result option
+  val force: 'a lazy -> 'a
+  val map_force: ('a -> 'a) -> 'a lazy -> 'a lazy
 end
 
 structure Lazy :> LAZY =
@@ -22,13 +22,13 @@
 
 (* datatype *)
 
-datatype 'a lazy =
+datatype 'a T =
   Lazy of unit -> 'a |
   Result of 'a Exn.result;
 
-type 'a T = 'a lazy ref;
+type 'a lazy = 'a T ref;
 
-fun same (r1: 'a T, r2) = r1 = r2;
+fun same (r1: 'a lazy, r2) = r1 = r2;
 
 fun lazy e = ref (Lazy e);
 fun value x = ref (Result (Exn.Result x));
@@ -58,3 +58,6 @@
 fun map_force f = value o f o force;
 
 end;
+
+type 'a lazy = 'a Lazy.lazy;
+
diff -r da79ac67794b -r 300ec36a19af src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Dec 02 14:29:12 2008 +0100
+++ b/src/Pure/Isar/code.ML	Thu Dec 04 23:00:21 2008 +0100
@@ -15,7 +15,7 @@
   val add_default_eqn_attrib: Attrib.src
   val del_eqn: thm -> theory -> theory
   val del_eqns: string -> theory -> theory
-  val add_eqnl: string * (thm * bool) list Lazy.T -> theory -> theory
+  val add_eqnl: string * (thm * bool) list lazy -> theory -> theory
   val map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
   val map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
   val add_inline: thm -> theory -> theory
@@ -114,7 +114,7 @@
 
 (* defining equations *)
 
-type eqns = bool * (thm * bool) list Lazy.T;
+type eqns = bool * (thm * bool) list lazy;
   (*default flag, theorems with linear flag (perhaps lazy)*)
 
 fun pretty_lthms ctxt r = case Lazy.peek r
diff -r da79ac67794b -r 300ec36a19af src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Dec 02 14:29:12 2008 +0100
+++ b/src/Pure/proofterm.ML	Thu Dec 04 23:00:21 2008 +0100
@@ -22,10 +22,10 @@
    | PAxm of string * term * typ list option
    | Oracle of string * term * typ list option
    | Promise of serial * term * typ list
-   | PThm of serial * ((string * term * typ list option) * proof_body Lazy.T)
+   | PThm of serial * ((string * term * typ list option) * proof_body lazy)
   and proof_body = PBody of
     {oracles: (string * term) OrdList.T,
-     thms: (serial * (string * term * proof_body Lazy.T)) OrdList.T,
+     thms: (serial * (string * term * proof_body lazy)) OrdList.T,
      proof: proof}
 
   val %> : proof * term -> proof
@@ -36,10 +36,10 @@
   include BASIC_PROOFTERM
 
   type oracle = string * term
-  type pthm = serial * (string * term * proof_body Lazy.T)
-  val force_body: proof_body Lazy.T ->
+  type pthm = serial * (string * term * proof_body lazy)
+  val force_body: proof_body lazy ->
     {oracles: oracle OrdList.T, thms: pthm OrdList.T, proof: proof}
-  val force_proof: proof_body Lazy.T -> proof
+  val force_proof: proof_body lazy -> proof
   val proof_of: proof_body -> proof
   val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
   val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
@@ -111,7 +111,7 @@
   val promise_proof: theory -> serial -> term -> proof
   val fulfill_proof: theory -> (serial * proof) list -> proof_body -> proof_body
   val thm_proof: theory -> string -> term list -> term ->
-    (serial * proof) list Lazy.T -> proof_body -> pthm * proof
+    (serial * proof) list lazy -> proof_body -> pthm * proof
   val get_name: term list -> term -> proof -> string
 
   (** rewriting on proof terms **)
@@ -143,14 +143,14 @@
  | PAxm of string * term * typ list option
  | Oracle of string * term * typ list option
  | Promise of serial * term * typ list
- | PThm of serial * ((string * term * typ list option) * proof_body Lazy.T)
+ | PThm of serial * ((string * term * typ list option) * proof_body lazy)
 and proof_body = PBody of
   {oracles: (string * term) OrdList.T,
-   thms: (serial * (string * term * proof_body Lazy.T)) OrdList.T,
+   thms: (serial * (string * term * proof_body lazy)) OrdList.T,
    proof: proof};
 
 type oracle = string * term;
-type pthm = serial * (string * term * proof_body Lazy.T);
+type pthm = serial * (string * term * proof_body lazy);
 
 val force_body = Lazy.force #> (fn PBody args => args);
 val force_proof = #proof o force_body;
diff -r da79ac67794b -r 300ec36a19af src/Tools/code/code_ml.ML
--- a/src/Tools/code/code_ml.ML	Tue Dec 02 14:29:12 2008 +0100
+++ b/src/Tools/code/code_ml.ML	Thu Dec 04 23:00:21 2008 +0100
@@ -912,7 +912,7 @@
 
 structure CodeAntiqData = ProofDataFun
 (
-  type T = string list * (bool * (string * (string * (string * string) list) Lazy.T));
+  type T = string list * (bool * (string * (string * (string * string) list) lazy));
   fun init _ = ([], (true, ("", Lazy.value ("", []))));
 );