src/Pure/Isar/code.ML

   val add_liberal_eqn: thm -> theory -> theory
   val add_default_eqn: thm -> theory -> theory
   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
   val del_inline: thm -> theory -> theory
   val add_post: thm -> theory -> theory

 
 (** logical and syntactical specification of executable code **)
 
 (* 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
     val args_of = snd o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
     val args = args_of thm;

       andalso matches_args (args_of thm') then 
         (warning ("Code generator: dropping redundant defining equation\n" ^ Display.string_of_thm thm'); true)
       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
   | merge_defthms ((false, _), defthms2 as (false, _)) = defthms2;
 

 
 
 (* 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
 };
 
 fun mk_spec (eqns, (dtyps, cases)) =

     val base_constraints = Sorts.mg_domain algebra tyco [class];
     val classparam_constraints = Sorts.complete_sort algebra [class]
       |> 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));
   in fold inter_sorts classparam_constraints base_constraints end;
 

             then error ("Rejected equation for datatype constructor:\n"
               ^ Display.string_of_thm thm)
             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;
 
 val add_eqn = gen_add_eqn true true false;
 val add_liberal_eqn = gen_add_eqn true false false;

  of SOME (thm, _) => let val c = Code_Unit.const_eqn thm
       in map_exec_purge (SOME [c]) (map_eqns (Symtab.map_entry c (del_thm thm))) thy end
   | 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
     val lthms' = certificate thy
       (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;
 
 val add_default_eqn_attr = Attrib.internal (fn _ => Thm.declaration_attribute
   (fn thm => Context.mapping (add_default_eqn thm) I));

 
 local
 
 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);
 
 fun apply_functrans thy c _ [] = []
   | apply_functrans thy c [] eqns = eqns