# HG changeset patch
# User wenzelm
# Date 1224764536 -7200
# Node ID d746a8c12c43f8afbc466a07626f167925e217f1
# Parent  0baf1d9c6780533fa3600d177cbbe731b1a23d7c
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;

diff -r 0baf1d9c6780 -r d746a8c12c43 doc-src/IsarAdvanced/Codegen/Thy/ML.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/ML.thy	Thu Oct 23 13:52:28 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/ML.thy	Thu Oct 23 14:22:16 2008 +0200
@@ -24,7 +24,7 @@
   \begin{mldecls}
   @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\
   @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\
-  @{index_ML Code.add_eqnl: "string * (thm * bool) list Susp.T -> theory -> theory"} \\
+  @{index_ML Code.add_eqnl: "string * (thm * bool) list Lazy.T -> theory -> theory"} \\
   @{index_ML Code.map_pre: "(MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory"} \\
   @{index_ML Code.map_post: "(MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory"} \\
   @{index_ML Code.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option)
diff -r 0baf1d9c6780 -r d746a8c12c43 src/HOL/Import/lazy_seq.ML
--- a/src/HOL/Import/lazy_seq.ML	Thu Oct 23 13:52:28 2008 +0200
+++ b/src/HOL/Import/lazy_seq.ML	Thu Oct 23 14:22:16 2008 +0200
@@ -80,13 +80,13 @@
 structure LazySeq :> LAZY_SEQ =
 struct
 
-datatype 'a seq = Seq of ('a * 'a seq) option Susp.T
+datatype 'a seq = Seq of ('a * 'a seq) option Lazy.T
 
 exception Empty
 
-fun getItem (Seq s) = Susp.force s
+fun getItem (Seq s) = Lazy.force s
 val pull = getItem
-fun make f = Seq (Susp.delay f)
+fun make f = Seq (Lazy.lazy f)
 
 fun null s = is_none (getItem s)
 
@@ -137,7 +137,7 @@
 local
     fun F NONE _ = raise Subscript
       | F (SOME(x,s)) n = SOME(x,F' s (n-1))
-    and F' s 0 = Seq (Susp.value NONE)
+    and F' s 0 = Seq (Lazy.value NONE)
       | F' s n = make (fn () => F (getItem s) n)
 in
 fun take (s,n) =
@@ -166,14 +166,14 @@
 
 local
     fun F s NONE = s
-      | F s (SOME(x,s')) = F (SOME(x, Seq (Susp.value s))) (getItem s')
+      | F s (SOME(x,s')) = F (SOME(x, Seq (Lazy.value s))) (getItem s')
 in
 fun rev s = make (fn () => F NONE (getItem s))
 end
 
 local
     fun F s NONE = getItem s
-      | F s (SOME(x,s')) = F (Seq (Susp.value (SOME(x,s)))) (getItem s')
+      | F s (SOME(x,s')) = F (Seq (Lazy.value (SOME(x,s)))) (getItem s')
 in
 fun revAppend (s1,s2) = make (fn () => F s2 (getItem s1))
 end
@@ -294,13 +294,13 @@
 	F' s1 s2
     end
 
-fun empty  _ = Seq (Susp.value NONE)
-fun single x = Seq(Susp.value (SOME(x,Seq (Susp.value NONE))))
-fun cons a = Seq(Susp.value (SOME a))
+fun empty  _ = Seq (Lazy.value NONE)
+fun single x = Seq(Lazy.value (SOME(x,Seq (Lazy.value NONE))))
+fun cons a = Seq(Lazy.value (SOME a))
 
 fun cycle seqfn =
     let
-	val knot = ref (Seq (Susp.value NONE))
+	val knot = ref (Seq (Lazy.value NONE))
     in
 	knot := seqfn (fn () => !knot);
 	!knot
@@ -374,7 +374,7 @@
 (* Adapted from seq.ML *)
 
 val succeed = single
-fun fail _ = Seq (Susp.value NONE)
+fun fail _ = Seq (Lazy.value NONE)
 
 (* fun op THEN (f, g) x = flat (map g (f x)) *)
 
@@ -414,7 +414,7 @@
 fun TRY f x =
     make (fn () =>
 	     case getItem (f x) of
-		 NONE => SOME(x,Seq (Susp.value NONE))
+		 NONE => SOME(x,Seq (Lazy.value NONE))
 	       | some => some)
 
 fun REPEAT f =
@@ -446,13 +446,13 @@
     make (fn () =>
 	     case getItem (f x) of
 		 NONE => NONE
-	       | SOME (x', _) => SOME(x',Seq (Susp.value NONE)))
+	       | SOME (x', _) => SOME(x',Seq (Lazy.value NONE)))
 
 (*partial function as procedure*)
 fun try f x =
     make (fn () =>
 	     case Basics.try f x of
-		 SOME y => SOME(y,Seq (Susp.value NONE))
+		 SOME y => SOME(y,Seq (Lazy.value NONE))
 	       | NONE => NONE)
 
 (*functional to print a sequence, up to "count" elements;
@@ -497,7 +497,7 @@
 
 (*turn a list of sequences into a sequence of lists*)
 local
-    fun F [] = SOME([],Seq (Susp.value NONE))
+    fun F [] = SOME([],Seq (Lazy.value NONE))
       | F (xq :: xqs) =
         case getItem xq of
             NONE => NONE
diff -r 0baf1d9c6780 -r d746a8c12c43 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Thu Oct 23 13:52:28 2008 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Thu Oct 23 14:22:16 2008 +0200
@@ -464,7 +464,7 @@
         fun get_thms () = (eq_refl, false)
           :: rev (map (rpair true) (get_eq' (Theory.deref thy_ref) dtco));
       in
-        Code.add_eqnl (const, Susp.delay get_thms) thy
+        Code.add_eqnl (const, Lazy.lazy get_thms) thy
       end;
   in
     thy
diff -r 0baf1d9c6780 -r d746a8c12c43 src/Pure/General/ROOT.ML
--- a/src/Pure/General/ROOT.ML	Thu Oct 23 13:52:28 2008 +0200
+++ b/src/Pure/General/ROOT.ML	Thu Oct 23 14:22:16 2008 +0200
@@ -28,7 +28,7 @@
 use "balanced_tree.ML";
 use "graph.ML";
 use "name_space.ML";
-use "susp.ML";
+use "lazy.ML";
 use "path.ML";
 use "url.ML";
 use "buffer.ML";
diff -r 0baf1d9c6780 -r d746a8c12c43 src/Pure/General/lazy.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/lazy.ML	Thu Oct 23 14:22:16 2008 +0200
@@ -0,0 +1,60 @@
+(*  Title:      Pure/General/lazy.ML
+    ID:         $Id$
+    Author:     Florian Haftmann and Makarius, TU Muenchen
+
+Lazy evaluation with memoing.  Concurrency may lead to multiple
+attempts of evaluation -- the first result persists.
+*)
+
+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
+end
+
+structure Lazy :> LAZY =
+struct
+
+(* datatype *)
+
+datatype 'a lazy =
+  Lazy of unit -> 'a |
+  Result of 'a Exn.result;
+
+type 'a T = 'a lazy ref;
+
+fun same (r1: 'a T, r2) = r1 = r2;
+
+fun lazy e = ref (Lazy e);
+fun value x = ref (Result (Exn.Result x));
+
+fun peek r =
+  (case ! r of
+    Lazy _ => NONE
+  | Result res => SOME res);
+
+
+(* force result *)
+
+fun force r =
+  let
+    (*potentially concurrent evaluation*)
+    val res =
+      (case ! r of
+        Lazy e => Exn.capture e ()
+      | Result res => res);
+    (*assign result -- first one persists*)
+    val res' = NAMED_CRITICAL "lazy" (fn () =>
+      (case ! r of
+        Lazy _ => (r := Result res; res)
+      | Result res' => res'));
+  in Exn.release res' end;
+
+fun map_force f = value o f o force;
+
+end;
diff -r 0baf1d9c6780 -r d746a8c12c43 src/Pure/General/susp.ML
--- a/src/Pure/General/susp.ML	Thu Oct 23 13:52:28 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(*  Title:      Pure/General/susp.ML
-    ID:         $Id$
-    Author:     Sebastian Skalberg, Florian Haftmann and Makarius, TU Muenchen
-
-Delayed evaluation with memoing.  Concurrency may lead to multiple
-attempts of evaluation -- the first result persists.
-*)
-
-signature SUSP =
-sig
-  type 'a T
-  val same: 'a T * 'a T -> bool
-  val delay: (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
-end
-
-structure Susp :> SUSP =
-struct
-
-(* datatype *)
-
-datatype 'a susp =
-  Delay of unit -> 'a |
-  Result of 'a Exn.result;
-
-type 'a T = 'a susp ref;
-
-fun same (r1: 'a T, r2) = r1 = r2;
-
-fun delay e = ref (Delay e);
-fun value x = ref (Result (Exn.Result x));
-
-fun peek r =
-  (case ! r of
-    Delay _ => NONE
-  | Result res => SOME res);
-
-
-(* force result *)
-
-fun force r =
-  let
-    (*potentially concurrent evaluation*)
-    val res =
-      (case ! r of
-        Delay e => Exn.capture e ()
-      | Result res => res);
-    (*assign result -- first one persists*)
-    val res' = NAMED_CRITICAL "susp" (fn () =>
-      (case ! r of
-        Delay _ => (r := Result res; res)
-      | Result res' => res'));
-  in Exn.release res' end;
-
-fun map_force f = value o f o force;
-
-end;
diff -r 0baf1d9c6780 -r d746a8c12c43 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Thu Oct 23 13:52:28 2008 +0200
+++ b/src/Pure/IsaMakefile	Thu Oct 23 14:22:16 2008 +0200
@@ -30,33 +30,34 @@
   Concurrent/task_queue.ML General/ROOT.ML General/alist.ML		\
   General/balanced_tree.ML General/basics.ML General/buffer.ML		\
   General/file.ML General/graph.ML General/heap.ML General/integer.ML	\
-  General/markup.ML General/name_space.ML General/ord_list.ML		\
-  General/output.ML General/path.ML General/position.ML			\
-  General/pretty.ML General/print_mode.ML General/properties.ML		\
-  General/queue.ML General/scan.ML General/secure.ML General/seq.ML	\
-  General/source.ML General/stack.ML General/susp.ML General/symbol.ML	\
-  General/symbol_pos.ML General/table.ML General/url.ML General/xml.ML	\
-  General/yxml.ML Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML		\
-  Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML	\
-  Isar/code.ML Isar/code_unit.ML Isar/constdefs.ML			\
-  Isar/context_rules.ML Isar/element.ML Isar/find_theorems.ML		\
-  Isar/instance.ML Isar/isar.ML Isar/isar_cmd.ML Isar/isar_syn.ML	\
-  Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML		\
-  Isar/locale.ML Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML	\
-  Isar/obtain.ML Isar/outer_keyword.ML Isar/outer_lex.ML		\
-  Isar/outer_parse.ML Isar/outer_syntax.ML Isar/overloading.ML		\
-  Isar/proof.ML Isar/proof_context.ML Isar/proof_display.ML		\
-  Isar/proof_node.ML Isar/rule_cases.ML Isar/rule_insts.ML		\
-  Isar/session.ML Isar/skip_proof.ML Isar/spec_parse.ML			\
-  Isar/specification.ML Isar/subclass.ML Isar/theory_target.ML		\
-  Isar/toplevel.ML ML-Systems/alice.ML ML-Systems/exn.ML		\
-  ML-Systems/install_pp_polyml.ML ML-Systems/ml_name_space.ML		\
-  ML-Systems/multithreading.ML ML-Systems/mosml.ML			\
-  ML-Systems/multithreading_polyml.ML ML-Systems/overloading_smlnj.ML	\
-  ML-Systems/polyml-4.1.3.ML ML-Systems/polyml-4.1.4.ML			\
-  ML-Systems/polyml-4.2.0.ML ML-Systems/polyml-5.0.ML			\
-  ML-Systems/polyml-5.1.ML ML-Systems/polyml_common.ML			\
-  ML-Systems/polyml.ML ML-Systems/polyml_old_compiler4.ML		\
+  General/lazy.ML General/markup.ML General/name_space.ML		\
+  General/ord_list.ML General/output.ML General/path.ML			\
+  General/position.ML General/pretty.ML General/print_mode.ML		\
+  General/properties.ML General/queue.ML General/scan.ML		\
+  General/secure.ML General/seq.ML General/source.ML General/stack.ML	\
+  General/symbol.ML General/symbol_pos.ML General/table.ML		\
+  General/url.ML General/xml.ML General/yxml.ML Isar/ROOT.ML		\
+  Isar/antiquote.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML	\
+  Isar/calculation.ML Isar/class.ML Isar/code.ML Isar/code_unit.ML	\
+  Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML		\
+  Isar/find_theorems.ML Isar/instance.ML Isar/isar.ML Isar/isar_cmd.ML	\
+  Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML		\
+  Isar/local_theory.ML Isar/locale.ML Isar/method.ML Isar/net_rules.ML	\
+  Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML		\
+  Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML		\
+  Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML		\
+  Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML		\
+  Isar/rule_insts.ML Isar/session.ML Isar/skip_proof.ML			\
+  Isar/spec_parse.ML Isar/specification.ML Isar/subclass.ML		\
+  Isar/theory_target.ML Isar/toplevel.ML ML-Systems/alice.ML		\
+  ML-Systems/exn.ML ML-Systems/install_pp_polyml.ML			\
+  ML-Systems/ml_name_space.ML ML-Systems/multithreading.ML		\
+  ML-Systems/mosml.ML ML-Systems/multithreading_polyml.ML		\
+  ML-Systems/overloading_smlnj.ML ML-Systems/polyml-4.1.3.ML		\
+  ML-Systems/polyml-4.1.4.ML ML-Systems/polyml-4.2.0.ML			\
+  ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML			\
+  ML-Systems/polyml_common.ML ML-Systems/polyml.ML			\
+  ML-Systems/polyml_old_compiler4.ML					\
   ML-Systems/polyml_old_compiler5.ML ML-Systems/proper_int.ML		\
   ML-Systems/smlnj.ML ML-Systems/system_shell.ML			\
   ML-Systems/time_limit.ML ML-Systems/thread_dummy.ML			\
diff -r 0baf1d9c6780 -r d746a8c12c43 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Thu Oct 23 13:52:28 2008 +0200
+++ b/src/Pure/Isar/code.ML	Thu Oct 23 14:22:16 2008 +0200
@@ -15,7 +15,7 @@
   val add_default_eqn_attr: Attrib.src
   val del_eqn: thm -> theory -> theory
   val del_eqns: string -> theory -> theory
-  val add_eqnl: string * (thm * bool) list Susp.T -> theory -> theory
+  val add_eqnl: string * (thm * bool) list Lazy.T -> 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
@@ -117,16 +117,16 @@
 
 (* defining equations with linear flag, default flag and lazy theorems *)
 
-fun pretty_lthms ctxt r = case Susp.peek r
+fun pretty_lthms ctxt r = case Lazy.peek r
  of SOME thms => map (ProofContext.pretty_thm ctxt o fst) (Exn.release thms)
   | NONE => [Pretty.str "[...]"];
 
 fun certificate thy f r =
-  case Susp.peek r
-   of SOME thms => (Susp.value o f thy) (Exn.release thms)
+  case Lazy.peek r
+   of SOME thms => (Lazy.value o f thy) (Exn.release thms)
     | NONE => let
         val thy_ref = Theory.check_thy thy;
-      in Susp.delay (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end;
+      in Lazy.lazy (fn () => (f (Theory.deref thy_ref) o Lazy.force) r) end;
 
 fun add_drop_redundant thy (thm, linear) thms =
   let
@@ -141,13 +141,13 @@
       else false;
   in (thm, linear) :: filter_out drop thms end;
 
-fun add_thm thy _ thm (false, thms) = (false, Susp.map_force (add_drop_redundant thy thm) thms)
-  | add_thm thy true thm (true, thms) = (true, Susp.map_force (fn thms => thms @ [thm]) thms)
-  | add_thm thy false thm (true, thms) = (false, Susp.value [thm]);
+fun add_thm thy _ thm (false, thms) = (false, Lazy.map_force (add_drop_redundant thy thm) thms)
+  | add_thm thy true thm (true, thms) = (true, Lazy.map_force (fn thms => thms @ [thm]) thms)
+  | add_thm thy false thm (true, thms) = (false, Lazy.value [thm]);
 
 fun add_lthms lthms _ = (false, lthms);
 
-fun del_thm thm = (apsnd o Susp.map_force) (remove (eq_fst Thm.eq_thm_prop) (thm, true));
+fun del_thm thm = (apsnd o Lazy.map_force) (remove (eq_fst Thm.eq_thm_prop) (thm, true));
 
 fun merge_defthms ((true, _), defthms2) = defthms2
   | merge_defthms (defthms1 as (false, _), (true, _)) = defthms1
@@ -171,7 +171,7 @@
 (* specification data *)
 
 datatype spec = Spec of {
-  eqns: (bool * (thm * bool) list Susp.T) Symtab.table,
+  eqns: (bool * (thm * bool) list Lazy.T) Symtab.table,
   dtyps: ((string * sort) list * (string * typ list) list) Symtab.table,
   cases: (int * string list) Symtab.table * unit Symtab.table
 };
@@ -471,7 +471,7 @@
       |> maps (map fst o these o try (#params o AxClass.get_info thy))
       |> map_filter (fn c => try (AxClass.param_of_inst thy) (c, tyco))
       |> map (Symtab.lookup ((the_eqns o the_exec) thy))
-      |> (map o Option.map) (map fst o Susp.force o snd)
+      |> (map o Option.map) (map fst o Lazy.force o snd)
       |> maps these
       |> map (map (snd o dest_TVar) o Sign.const_typargs thy o Code_Unit.const_typ_eqn);
     val inter_sorts = map2 (curry (Sorts.inter_sort algebra));
@@ -544,7 +544,7 @@
             else ();
         in
           (map_exec_purge (SOME [c]) o map_eqns) (Symtab.map_default
-            (c, (true, Susp.value [])) (add_thm thy default (thm, linear))) thy
+            (c, (true, Lazy.value [])) (add_thm thy default (thm, linear))) thy
         end
     | NONE => thy;
 
@@ -559,7 +559,7 @@
   | NONE => thy;
 
 fun del_eqns c = map_exec_purge (SOME [c])
-  (map_eqns (Symtab.map_entry c (K (false, Susp.value []))));
+  (map_eqns (Symtab.map_entry c (K (false, Lazy.value []))));
 
 fun add_eqnl (c, lthms) thy =
   let
@@ -567,7 +567,7 @@
       (fn thy => map (Code_Unit.assert_linear) o certify_const thy c) lthms;
   in
     map_exec_purge (SOME [c])
-      (map_eqns (Symtab.map_default (c, (true, Susp.value []))
+      (map_eqns (Symtab.map_default (c, (true, Lazy.value []))
         (add_lthms lthms'))) thy
   end;
 
@@ -648,7 +648,7 @@
 
 fun get_eqns thy c =
   Symtab.lookup ((the_eqns o the_exec) thy) c
-  |> Option.map (Susp.force o snd)
+  |> Option.map (Lazy.force o snd)
   |> these
   |> (map o apfst) (Thm.transfer thy);
 
diff -r 0baf1d9c6780 -r d746a8c12c43 src/Pure/ML-Systems/install_pp_polyml.ML
--- a/src/Pure/ML-Systems/install_pp_polyml.ML	Thu Oct 23 13:52:28 2008 +0200
+++ b/src/Pure/ML-Systems/install_pp_polyml.ML	Thu Oct 23 14:22:16 2008 +0200
@@ -10,9 +10,9 @@
   | SOME (Exn.Exn _) => str "<failed>"
   | SOME (Exn.Result y) => print (y, depth)));
 
-install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a Susp.T) =>
-  (case Susp.peek x of
-    NONE => str "<delayed>"
+install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a Lazy.T) =>
+  (case Lazy.peek x of
+    NONE => str "<lazy>"
   | SOME (Exn.Exn _) => str "<failed>"
   | SOME (Exn.Result y) => print (y, depth)));
 
diff -r 0baf1d9c6780 -r d746a8c12c43 src/Tools/code/code_ml.ML
--- a/src/Tools/code/code_ml.ML	Thu Oct 23 13:52:28 2008 +0200
+++ b/src/Tools/code/code_ml.ML	Thu Oct 23 14:22:16 2008 +0200
@@ -915,8 +915,8 @@
 
 structure CodeAntiqData = ProofDataFun
 (
-  type T = string list * (bool * (string * (string * (string * string) list) Susp.T));
-  fun init _ = ([], (true, ("", Susp.value ("", []))));
+  type T = string list * (bool * (string * (string * (string * string) list) Lazy.T));
+  fun init _ = ([], (true, ("", Lazy.value ("", []))));
 );
 
 val is_first_occ = fst o snd o CodeAntiqData.get;
@@ -938,13 +938,13 @@
     val (struct_name', ctxt') = if struct_name = ""
       then ML_Antiquote.variant "Code" ctxt
       else (struct_name, ctxt);
-    val acc_code = Susp.delay (delayed_code (ProofContext.theory_of ctxt) consts');
+    val acc_code = Lazy.lazy (delayed_code (ProofContext.theory_of ctxt) consts');
   in CodeAntiqData.put (consts', (false, (struct_name', acc_code))) ctxt' end;
 
 fun print_code struct_name is_first const ctxt =
   let
     val (consts, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
-    val (raw_ml_code, consts_map) = Susp.force acc_code;
+    val (raw_ml_code, consts_map) = Lazy.force acc_code;
     val const'' = NameSpace.append (NameSpace.append struct_name struct_code_name)
       ((the o AList.lookup (op =) consts_map) const);
     val ml_code = if is_first then "\nstructure " ^ struct_code_name