renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
authorwenzelm
Thu Oct 23 14:22:16 2008 +0200 (2008-10-23)
changeset 28673d746a8c12c43
parent 28672 0baf1d9c6780
child 28674 08a77c495dc1
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
doc-src/IsarAdvanced/Codegen/Thy/ML.thy
src/HOL/Import/lazy_seq.ML
src/HOL/Tools/datatype_codegen.ML
src/Pure/General/ROOT.ML
src/Pure/General/lazy.ML
src/Pure/General/susp.ML
src/Pure/IsaMakefile
src/Pure/Isar/code.ML
src/Pure/ML-Systems/install_pp_polyml.ML
src/Tools/code/code_ml.ML
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/ML.thy	Thu Oct 23 13:52:28 2008 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/ML.thy	Thu Oct 23 14:22:16 2008 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4    \begin{mldecls}
     1.5    @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\
     1.6    @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\
     1.7 -  @{index_ML Code.add_eqnl: "string * (thm * bool) list Susp.T -> theory -> theory"} \\
     1.8 +  @{index_ML Code.add_eqnl: "string * (thm * bool) list Lazy.T -> theory -> theory"} \\
     1.9    @{index_ML Code.map_pre: "(MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory"} \\
    1.10    @{index_ML Code.map_post: "(MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory"} \\
    1.11    @{index_ML Code.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option)
     2.1 --- a/src/HOL/Import/lazy_seq.ML	Thu Oct 23 13:52:28 2008 +0200
     2.2 +++ b/src/HOL/Import/lazy_seq.ML	Thu Oct 23 14:22:16 2008 +0200
     2.3 @@ -80,13 +80,13 @@
     2.4  structure LazySeq :> LAZY_SEQ =
     2.5  struct
     2.6  
     2.7 -datatype 'a seq = Seq of ('a * 'a seq) option Susp.T
     2.8 +datatype 'a seq = Seq of ('a * 'a seq) option Lazy.T
     2.9  
    2.10  exception Empty
    2.11  
    2.12 -fun getItem (Seq s) = Susp.force s
    2.13 +fun getItem (Seq s) = Lazy.force s
    2.14  val pull = getItem
    2.15 -fun make f = Seq (Susp.delay f)
    2.16 +fun make f = Seq (Lazy.lazy f)
    2.17  
    2.18  fun null s = is_none (getItem s)
    2.19  
    2.20 @@ -137,7 +137,7 @@
    2.21  local
    2.22      fun F NONE _ = raise Subscript
    2.23        | F (SOME(x,s)) n = SOME(x,F' s (n-1))
    2.24 -    and F' s 0 = Seq (Susp.value NONE)
    2.25 +    and F' s 0 = Seq (Lazy.value NONE)
    2.26        | F' s n = make (fn () => F (getItem s) n)
    2.27  in
    2.28  fun take (s,n) =
    2.29 @@ -166,14 +166,14 @@
    2.30  
    2.31  local
    2.32      fun F s NONE = s
    2.33 -      | F s (SOME(x,s')) = F (SOME(x, Seq (Susp.value s))) (getItem s')
    2.34 +      | F s (SOME(x,s')) = F (SOME(x, Seq (Lazy.value s))) (getItem s')
    2.35  in
    2.36  fun rev s = make (fn () => F NONE (getItem s))
    2.37  end
    2.38  
    2.39  local
    2.40      fun F s NONE = getItem s
    2.41 -      | F s (SOME(x,s')) = F (Seq (Susp.value (SOME(x,s)))) (getItem s')
    2.42 +      | F s (SOME(x,s')) = F (Seq (Lazy.value (SOME(x,s)))) (getItem s')
    2.43  in
    2.44  fun revAppend (s1,s2) = make (fn () => F s2 (getItem s1))
    2.45  end
    2.46 @@ -294,13 +294,13 @@
    2.47  	F' s1 s2
    2.48      end
    2.49  
    2.50 -fun empty  _ = Seq (Susp.value NONE)
    2.51 -fun single x = Seq(Susp.value (SOME(x,Seq (Susp.value NONE))))
    2.52 -fun cons a = Seq(Susp.value (SOME a))
    2.53 +fun empty  _ = Seq (Lazy.value NONE)
    2.54 +fun single x = Seq(Lazy.value (SOME(x,Seq (Lazy.value NONE))))
    2.55 +fun cons a = Seq(Lazy.value (SOME a))
    2.56  
    2.57  fun cycle seqfn =
    2.58      let
    2.59 -	val knot = ref (Seq (Susp.value NONE))
    2.60 +	val knot = ref (Seq (Lazy.value NONE))
    2.61      in
    2.62  	knot := seqfn (fn () => !knot);
    2.63  	!knot
    2.64 @@ -374,7 +374,7 @@
    2.65  (* Adapted from seq.ML *)
    2.66  
    2.67  val succeed = single
    2.68 -fun fail _ = Seq (Susp.value NONE)
    2.69 +fun fail _ = Seq (Lazy.value NONE)
    2.70  
    2.71  (* fun op THEN (f, g) x = flat (map g (f x)) *)
    2.72  
    2.73 @@ -414,7 +414,7 @@
    2.74  fun TRY f x =
    2.75      make (fn () =>
    2.76  	     case getItem (f x) of
    2.77 -		 NONE => SOME(x,Seq (Susp.value NONE))
    2.78 +		 NONE => SOME(x,Seq (Lazy.value NONE))
    2.79  	       | some => some)
    2.80  
    2.81  fun REPEAT f =
    2.82 @@ -446,13 +446,13 @@
    2.83      make (fn () =>
    2.84  	     case getItem (f x) of
    2.85  		 NONE => NONE
    2.86 -	       | SOME (x', _) => SOME(x',Seq (Susp.value NONE)))
    2.87 +	       | SOME (x', _) => SOME(x',Seq (Lazy.value NONE)))
    2.88  
    2.89  (*partial function as procedure*)
    2.90  fun try f x =
    2.91      make (fn () =>
    2.92  	     case Basics.try f x of
    2.93 -		 SOME y => SOME(y,Seq (Susp.value NONE))
    2.94 +		 SOME y => SOME(y,Seq (Lazy.value NONE))
    2.95  	       | NONE => NONE)
    2.96  
    2.97  (*functional to print a sequence, up to "count" elements;
    2.98 @@ -497,7 +497,7 @@
    2.99  
   2.100  (*turn a list of sequences into a sequence of lists*)
   2.101  local
   2.102 -    fun F [] = SOME([],Seq (Susp.value NONE))
   2.103 +    fun F [] = SOME([],Seq (Lazy.value NONE))
   2.104        | F (xq :: xqs) =
   2.105          case getItem xq of
   2.106              NONE => NONE
     3.1 --- a/src/HOL/Tools/datatype_codegen.ML	Thu Oct 23 13:52:28 2008 +0200
     3.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Thu Oct 23 14:22:16 2008 +0200
     3.3 @@ -464,7 +464,7 @@
     3.4          fun get_thms () = (eq_refl, false)
     3.5            :: rev (map (rpair true) (get_eq' (Theory.deref thy_ref) dtco));
     3.6        in
     3.7 -        Code.add_eqnl (const, Susp.delay get_thms) thy
     3.8 +        Code.add_eqnl (const, Lazy.lazy get_thms) thy
     3.9        end;
    3.10    in
    3.11      thy
     4.1 --- a/src/Pure/General/ROOT.ML	Thu Oct 23 13:52:28 2008 +0200
     4.2 +++ b/src/Pure/General/ROOT.ML	Thu Oct 23 14:22:16 2008 +0200
     4.3 @@ -28,7 +28,7 @@
     4.4  use "balanced_tree.ML";
     4.5  use "graph.ML";
     4.6  use "name_space.ML";
     4.7 -use "susp.ML";
     4.8 +use "lazy.ML";
     4.9  use "path.ML";
    4.10  use "url.ML";
    4.11  use "buffer.ML";
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/General/lazy.ML	Thu Oct 23 14:22:16 2008 +0200
     5.3 @@ -0,0 +1,60 @@
     5.4 +(*  Title:      Pure/General/lazy.ML
     5.5 +    ID:         $Id$
     5.6 +    Author:     Florian Haftmann and Makarius, TU Muenchen
     5.7 +
     5.8 +Lazy evaluation with memoing.  Concurrency may lead to multiple
     5.9 +attempts of evaluation -- the first result persists.
    5.10 +*)
    5.11 +
    5.12 +signature LAZY =
    5.13 +sig
    5.14 +  type 'a T
    5.15 +  val same: 'a T * 'a T -> bool
    5.16 +  val lazy: (unit -> 'a) -> 'a T
    5.17 +  val value: 'a -> 'a T
    5.18 +  val peek: 'a T -> 'a Exn.result option
    5.19 +  val force: 'a T -> 'a
    5.20 +  val map_force: ('a -> 'a) -> 'a T -> 'a T
    5.21 +end
    5.22 +
    5.23 +structure Lazy :> LAZY =
    5.24 +struct
    5.25 +
    5.26 +(* datatype *)
    5.27 +
    5.28 +datatype 'a lazy =
    5.29 +  Lazy of unit -> 'a |
    5.30 +  Result of 'a Exn.result;
    5.31 +
    5.32 +type 'a T = 'a lazy ref;
    5.33 +
    5.34 +fun same (r1: 'a T, r2) = r1 = r2;
    5.35 +
    5.36 +fun lazy e = ref (Lazy e);
    5.37 +fun value x = ref (Result (Exn.Result x));
    5.38 +
    5.39 +fun peek r =
    5.40 +  (case ! r of
    5.41 +    Lazy _ => NONE
    5.42 +  | Result res => SOME res);
    5.43 +
    5.44 +
    5.45 +(* force result *)
    5.46 +
    5.47 +fun force r =
    5.48 +  let
    5.49 +    (*potentially concurrent evaluation*)
    5.50 +    val res =
    5.51 +      (case ! r of
    5.52 +        Lazy e => Exn.capture e ()
    5.53 +      | Result res => res);
    5.54 +    (*assign result -- first one persists*)
    5.55 +    val res' = NAMED_CRITICAL "lazy" (fn () =>
    5.56 +      (case ! r of
    5.57 +        Lazy _ => (r := Result res; res)
    5.58 +      | Result res' => res'));
    5.59 +  in Exn.release res' end;
    5.60 +
    5.61 +fun map_force f = value o f o force;
    5.62 +
    5.63 +end;
     6.1 --- a/src/Pure/General/susp.ML	Thu Oct 23 13:52:28 2008 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,60 +0,0 @@
     6.4 -(*  Title:      Pure/General/susp.ML
     6.5 -    ID:         $Id$
     6.6 -    Author:     Sebastian Skalberg, Florian Haftmann and Makarius, TU Muenchen
     6.7 -
     6.8 -Delayed evaluation with memoing.  Concurrency may lead to multiple
     6.9 -attempts of evaluation -- the first result persists.
    6.10 -*)
    6.11 -
    6.12 -signature SUSP =
    6.13 -sig
    6.14 -  type 'a T
    6.15 -  val same: 'a T * 'a T -> bool
    6.16 -  val delay: (unit -> 'a) -> 'a T
    6.17 -  val value: 'a -> 'a T
    6.18 -  val peek: 'a T -> 'a Exn.result option
    6.19 -  val force: 'a T -> 'a
    6.20 -  val map_force: ('a -> 'a) -> 'a T -> 'a T
    6.21 -end
    6.22 -
    6.23 -structure Susp :> SUSP =
    6.24 -struct
    6.25 -
    6.26 -(* datatype *)
    6.27 -
    6.28 -datatype 'a susp =
    6.29 -  Delay of unit -> 'a |
    6.30 -  Result of 'a Exn.result;
    6.31 -
    6.32 -type 'a T = 'a susp ref;
    6.33 -
    6.34 -fun same (r1: 'a T, r2) = r1 = r2;
    6.35 -
    6.36 -fun delay e = ref (Delay e);
    6.37 -fun value x = ref (Result (Exn.Result x));
    6.38 -
    6.39 -fun peek r =
    6.40 -  (case ! r of
    6.41 -    Delay _ => NONE
    6.42 -  | Result res => SOME res);
    6.43 -
    6.44 -
    6.45 -(* force result *)
    6.46 -
    6.47 -fun force r =
    6.48 -  let
    6.49 -    (*potentially concurrent evaluation*)
    6.50 -    val res =
    6.51 -      (case ! r of
    6.52 -        Delay e => Exn.capture e ()
    6.53 -      | Result res => res);
    6.54 -    (*assign result -- first one persists*)
    6.55 -    val res' = NAMED_CRITICAL "susp" (fn () =>
    6.56 -      (case ! r of
    6.57 -        Delay _ => (r := Result res; res)
    6.58 -      | Result res' => res'));
    6.59 -  in Exn.release res' end;
    6.60 -
    6.61 -fun map_force f = value o f o force;
    6.62 -
    6.63 -end;
     7.1 --- a/src/Pure/IsaMakefile	Thu Oct 23 13:52:28 2008 +0200
     7.2 +++ b/src/Pure/IsaMakefile	Thu Oct 23 14:22:16 2008 +0200
     7.3 @@ -30,33 +30,34 @@
     7.4    Concurrent/task_queue.ML General/ROOT.ML General/alist.ML		\
     7.5    General/balanced_tree.ML General/basics.ML General/buffer.ML		\
     7.6    General/file.ML General/graph.ML General/heap.ML General/integer.ML	\
     7.7 -  General/markup.ML General/name_space.ML General/ord_list.ML		\
     7.8 -  General/output.ML General/path.ML General/position.ML			\
     7.9 -  General/pretty.ML General/print_mode.ML General/properties.ML		\
    7.10 -  General/queue.ML General/scan.ML General/secure.ML General/seq.ML	\
    7.11 -  General/source.ML General/stack.ML General/susp.ML General/symbol.ML	\
    7.12 -  General/symbol_pos.ML General/table.ML General/url.ML General/xml.ML	\
    7.13 -  General/yxml.ML Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML		\
    7.14 -  Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML	\
    7.15 -  Isar/code.ML Isar/code_unit.ML Isar/constdefs.ML			\
    7.16 -  Isar/context_rules.ML Isar/element.ML Isar/find_theorems.ML		\
    7.17 -  Isar/instance.ML Isar/isar.ML Isar/isar_cmd.ML Isar/isar_syn.ML	\
    7.18 -  Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML		\
    7.19 -  Isar/locale.ML Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML	\
    7.20 -  Isar/obtain.ML Isar/outer_keyword.ML Isar/outer_lex.ML		\
    7.21 -  Isar/outer_parse.ML Isar/outer_syntax.ML Isar/overloading.ML		\
    7.22 -  Isar/proof.ML Isar/proof_context.ML Isar/proof_display.ML		\
    7.23 -  Isar/proof_node.ML Isar/rule_cases.ML Isar/rule_insts.ML		\
    7.24 -  Isar/session.ML Isar/skip_proof.ML Isar/spec_parse.ML			\
    7.25 -  Isar/specification.ML Isar/subclass.ML Isar/theory_target.ML		\
    7.26 -  Isar/toplevel.ML ML-Systems/alice.ML ML-Systems/exn.ML		\
    7.27 -  ML-Systems/install_pp_polyml.ML ML-Systems/ml_name_space.ML		\
    7.28 -  ML-Systems/multithreading.ML ML-Systems/mosml.ML			\
    7.29 -  ML-Systems/multithreading_polyml.ML ML-Systems/overloading_smlnj.ML	\
    7.30 -  ML-Systems/polyml-4.1.3.ML ML-Systems/polyml-4.1.4.ML			\
    7.31 -  ML-Systems/polyml-4.2.0.ML ML-Systems/polyml-5.0.ML			\
    7.32 -  ML-Systems/polyml-5.1.ML ML-Systems/polyml_common.ML			\
    7.33 -  ML-Systems/polyml.ML ML-Systems/polyml_old_compiler4.ML		\
    7.34 +  General/lazy.ML General/markup.ML General/name_space.ML		\
    7.35 +  General/ord_list.ML General/output.ML General/path.ML			\
    7.36 +  General/position.ML General/pretty.ML General/print_mode.ML		\
    7.37 +  General/properties.ML General/queue.ML General/scan.ML		\
    7.38 +  General/secure.ML General/seq.ML General/source.ML General/stack.ML	\
    7.39 +  General/symbol.ML General/symbol_pos.ML General/table.ML		\
    7.40 +  General/url.ML General/xml.ML General/yxml.ML Isar/ROOT.ML		\
    7.41 +  Isar/antiquote.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML	\
    7.42 +  Isar/calculation.ML Isar/class.ML Isar/code.ML Isar/code_unit.ML	\
    7.43 +  Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML		\
    7.44 +  Isar/find_theorems.ML Isar/instance.ML Isar/isar.ML Isar/isar_cmd.ML	\
    7.45 +  Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML		\
    7.46 +  Isar/local_theory.ML Isar/locale.ML Isar/method.ML Isar/net_rules.ML	\
    7.47 +  Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML		\
    7.48 +  Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML		\
    7.49 +  Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML		\
    7.50 +  Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML		\
    7.51 +  Isar/rule_insts.ML Isar/session.ML Isar/skip_proof.ML			\
    7.52 +  Isar/spec_parse.ML Isar/specification.ML Isar/subclass.ML		\
    7.53 +  Isar/theory_target.ML Isar/toplevel.ML ML-Systems/alice.ML		\
    7.54 +  ML-Systems/exn.ML ML-Systems/install_pp_polyml.ML			\
    7.55 +  ML-Systems/ml_name_space.ML ML-Systems/multithreading.ML		\
    7.56 +  ML-Systems/mosml.ML ML-Systems/multithreading_polyml.ML		\
    7.57 +  ML-Systems/overloading_smlnj.ML ML-Systems/polyml-4.1.3.ML		\
    7.58 +  ML-Systems/polyml-4.1.4.ML ML-Systems/polyml-4.2.0.ML			\
    7.59 +  ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML			\
    7.60 +  ML-Systems/polyml_common.ML ML-Systems/polyml.ML			\
    7.61 +  ML-Systems/polyml_old_compiler4.ML					\
    7.62    ML-Systems/polyml_old_compiler5.ML ML-Systems/proper_int.ML		\
    7.63    ML-Systems/smlnj.ML ML-Systems/system_shell.ML			\
    7.64    ML-Systems/time_limit.ML ML-Systems/thread_dummy.ML			\
     8.1 --- a/src/Pure/Isar/code.ML	Thu Oct 23 13:52:28 2008 +0200
     8.2 +++ b/src/Pure/Isar/code.ML	Thu Oct 23 14:22:16 2008 +0200
     8.3 @@ -15,7 +15,7 @@
     8.4    val add_default_eqn_attr: Attrib.src
     8.5    val del_eqn: thm -> theory -> theory
     8.6    val del_eqns: string -> theory -> theory
     8.7 -  val add_eqnl: string * (thm * bool) list Susp.T -> theory -> theory
     8.8 +  val add_eqnl: string * (thm * bool) list Lazy.T -> theory -> theory
     8.9    val map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
    8.10    val map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
    8.11    val add_inline: thm -> theory -> theory
    8.12 @@ -117,16 +117,16 @@
    8.13  
    8.14  (* defining equations with linear flag, default flag and lazy theorems *)
    8.15  
    8.16 -fun pretty_lthms ctxt r = case Susp.peek r
    8.17 +fun pretty_lthms ctxt r = case Lazy.peek r
    8.18   of SOME thms => map (ProofContext.pretty_thm ctxt o fst) (Exn.release thms)
    8.19    | NONE => [Pretty.str "[...]"];
    8.20  
    8.21  fun certificate thy f r =
    8.22 -  case Susp.peek r
    8.23 -   of SOME thms => (Susp.value o f thy) (Exn.release thms)
    8.24 +  case Lazy.peek r
    8.25 +   of SOME thms => (Lazy.value o f thy) (Exn.release thms)
    8.26      | NONE => let
    8.27          val thy_ref = Theory.check_thy thy;
    8.28 -      in Susp.delay (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end;
    8.29 +      in Lazy.lazy (fn () => (f (Theory.deref thy_ref) o Lazy.force) r) end;
    8.30  
    8.31  fun add_drop_redundant thy (thm, linear) thms =
    8.32    let
    8.33 @@ -141,13 +141,13 @@
    8.34        else false;
    8.35    in (thm, linear) :: filter_out drop thms end;
    8.36  
    8.37 -fun add_thm thy _ thm (false, thms) = (false, Susp.map_force (add_drop_redundant thy thm) thms)
    8.38 -  | add_thm thy true thm (true, thms) = (true, Susp.map_force (fn thms => thms @ [thm]) thms)
    8.39 -  | add_thm thy false thm (true, thms) = (false, Susp.value [thm]);
    8.40 +fun add_thm thy _ thm (false, thms) = (false, Lazy.map_force (add_drop_redundant thy thm) thms)
    8.41 +  | add_thm thy true thm (true, thms) = (true, Lazy.map_force (fn thms => thms @ [thm]) thms)
    8.42 +  | add_thm thy false thm (true, thms) = (false, Lazy.value [thm]);
    8.43  
    8.44  fun add_lthms lthms _ = (false, lthms);
    8.45  
    8.46 -fun del_thm thm = (apsnd o Susp.map_force) (remove (eq_fst Thm.eq_thm_prop) (thm, true));
    8.47 +fun del_thm thm = (apsnd o Lazy.map_force) (remove (eq_fst Thm.eq_thm_prop) (thm, true));
    8.48  
    8.49  fun merge_defthms ((true, _), defthms2) = defthms2
    8.50    | merge_defthms (defthms1 as (false, _), (true, _)) = defthms1
    8.51 @@ -171,7 +171,7 @@
    8.52  (* specification data *)
    8.53  
    8.54  datatype spec = Spec of {
    8.55 -  eqns: (bool * (thm * bool) list Susp.T) Symtab.table,
    8.56 +  eqns: (bool * (thm * bool) list Lazy.T) Symtab.table,
    8.57    dtyps: ((string * sort) list * (string * typ list) list) Symtab.table,
    8.58    cases: (int * string list) Symtab.table * unit Symtab.table
    8.59  };
    8.60 @@ -471,7 +471,7 @@
    8.61        |> maps (map fst o these o try (#params o AxClass.get_info thy))
    8.62        |> map_filter (fn c => try (AxClass.param_of_inst thy) (c, tyco))
    8.63        |> map (Symtab.lookup ((the_eqns o the_exec) thy))
    8.64 -      |> (map o Option.map) (map fst o Susp.force o snd)
    8.65 +      |> (map o Option.map) (map fst o Lazy.force o snd)
    8.66        |> maps these
    8.67        |> map (map (snd o dest_TVar) o Sign.const_typargs thy o Code_Unit.const_typ_eqn);
    8.68      val inter_sorts = map2 (curry (Sorts.inter_sort algebra));
    8.69 @@ -544,7 +544,7 @@
    8.70              else ();
    8.71          in
    8.72            (map_exec_purge (SOME [c]) o map_eqns) (Symtab.map_default
    8.73 -            (c, (true, Susp.value [])) (add_thm thy default (thm, linear))) thy
    8.74 +            (c, (true, Lazy.value [])) (add_thm thy default (thm, linear))) thy
    8.75          end
    8.76      | NONE => thy;
    8.77  
    8.78 @@ -559,7 +559,7 @@
    8.79    | NONE => thy;
    8.80  
    8.81  fun del_eqns c = map_exec_purge (SOME [c])
    8.82 -  (map_eqns (Symtab.map_entry c (K (false, Susp.value []))));
    8.83 +  (map_eqns (Symtab.map_entry c (K (false, Lazy.value []))));
    8.84  
    8.85  fun add_eqnl (c, lthms) thy =
    8.86    let
    8.87 @@ -567,7 +567,7 @@
    8.88        (fn thy => map (Code_Unit.assert_linear) o certify_const thy c) lthms;
    8.89    in
    8.90      map_exec_purge (SOME [c])
    8.91 -      (map_eqns (Symtab.map_default (c, (true, Susp.value []))
    8.92 +      (map_eqns (Symtab.map_default (c, (true, Lazy.value []))
    8.93          (add_lthms lthms'))) thy
    8.94    end;
    8.95  
    8.96 @@ -648,7 +648,7 @@
    8.97  
    8.98  fun get_eqns thy c =
    8.99    Symtab.lookup ((the_eqns o the_exec) thy) c
   8.100 -  |> Option.map (Susp.force o snd)
   8.101 +  |> Option.map (Lazy.force o snd)
   8.102    |> these
   8.103    |> (map o apfst) (Thm.transfer thy);
   8.104  
     9.1 --- a/src/Pure/ML-Systems/install_pp_polyml.ML	Thu Oct 23 13:52:28 2008 +0200
     9.2 +++ b/src/Pure/ML-Systems/install_pp_polyml.ML	Thu Oct 23 14:22:16 2008 +0200
     9.3 @@ -10,9 +10,9 @@
     9.4    | SOME (Exn.Exn _) => str "<failed>"
     9.5    | SOME (Exn.Result y) => print (y, depth)));
     9.6  
     9.7 -install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a Susp.T) =>
     9.8 -  (case Susp.peek x of
     9.9 -    NONE => str "<delayed>"
    9.10 +install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a Lazy.T) =>
    9.11 +  (case Lazy.peek x of
    9.12 +    NONE => str "<lazy>"
    9.13    | SOME (Exn.Exn _) => str "<failed>"
    9.14    | SOME (Exn.Result y) => print (y, depth)));
    9.15  
    10.1 --- a/src/Tools/code/code_ml.ML	Thu Oct 23 13:52:28 2008 +0200
    10.2 +++ b/src/Tools/code/code_ml.ML	Thu Oct 23 14:22:16 2008 +0200
    10.3 @@ -915,8 +915,8 @@
    10.4  
    10.5  structure CodeAntiqData = ProofDataFun
    10.6  (
    10.7 -  type T = string list * (bool * (string * (string * (string * string) list) Susp.T));
    10.8 -  fun init _ = ([], (true, ("", Susp.value ("", []))));
    10.9 +  type T = string list * (bool * (string * (string * (string * string) list) Lazy.T));
   10.10 +  fun init _ = ([], (true, ("", Lazy.value ("", []))));
   10.11  );
   10.12  
   10.13  val is_first_occ = fst o snd o CodeAntiqData.get;
   10.14 @@ -938,13 +938,13 @@
   10.15      val (struct_name', ctxt') = if struct_name = ""
   10.16        then ML_Antiquote.variant "Code" ctxt
   10.17        else (struct_name, ctxt);
   10.18 -    val acc_code = Susp.delay (delayed_code (ProofContext.theory_of ctxt) consts');
   10.19 +    val acc_code = Lazy.lazy (delayed_code (ProofContext.theory_of ctxt) consts');
   10.20    in CodeAntiqData.put (consts', (false, (struct_name', acc_code))) ctxt' end;
   10.21  
   10.22  fun print_code struct_name is_first const ctxt =
   10.23    let
   10.24      val (consts, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
   10.25 -    val (raw_ml_code, consts_map) = Susp.force acc_code;
   10.26 +    val (raw_ml_code, consts_map) = Lazy.force acc_code;
   10.27      val const'' = NameSpace.append (NameSpace.append struct_name struct_code_name)
   10.28        ((the o AList.lookup (op =) consts_map) const);
   10.29      val ml_code = if is_first then "\nstructure " ^ struct_code_name