src/Tools/code/code_ml.ML
changeset 28673 d746a8c12c43
parent 28663 bd8438543bf2
child 28705 c77a9f5672f8
     1.1 --- a/src/Tools/code/code_ml.ML	Thu Oct 23 13:52:28 2008 +0200
     1.2 +++ b/src/Tools/code/code_ml.ML	Thu Oct 23 14:22:16 2008 +0200
     1.3 @@ -915,8 +915,8 @@
     1.4  
     1.5  structure CodeAntiqData = ProofDataFun
     1.6  (
     1.7 -  type T = string list * (bool * (string * (string * (string * string) list) Susp.T));
     1.8 -  fun init _ = ([], (true, ("", Susp.value ("", []))));
     1.9 +  type T = string list * (bool * (string * (string * (string * string) list) Lazy.T));
    1.10 +  fun init _ = ([], (true, ("", Lazy.value ("", []))));
    1.11  );
    1.12  
    1.13  val is_first_occ = fst o snd o CodeAntiqData.get;
    1.14 @@ -938,13 +938,13 @@
    1.15      val (struct_name', ctxt') = if struct_name = ""
    1.16        then ML_Antiquote.variant "Code" ctxt
    1.17        else (struct_name, ctxt);
    1.18 -    val acc_code = Susp.delay (delayed_code (ProofContext.theory_of ctxt) consts');
    1.19 +    val acc_code = Lazy.lazy (delayed_code (ProofContext.theory_of ctxt) consts');
    1.20    in CodeAntiqData.put (consts', (false, (struct_name', acc_code))) ctxt' end;
    1.21  
    1.22  fun print_code struct_name is_first const ctxt =
    1.23    let
    1.24      val (consts, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
    1.25 -    val (raw_ml_code, consts_map) = Susp.force acc_code;
    1.26 +    val (raw_ml_code, consts_map) = Lazy.force acc_code;
    1.27      val const'' = NameSpace.append (NameSpace.append struct_name struct_code_name)
    1.28        ((the o AList.lookup (op =) consts_map) const);
    1.29      val ml_code = if is_first then "\nstructure " ^ struct_code_name