--- 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);