isabelle: src/Pure/ML/ml_heap.ML@291cc01f56f5 (annotated)

62508 d0b68218ea55 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM; wenzelm parents: 62468 diff changeset	1	(* Title: Pure/ML/ml_heap.ML
62467 c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	2	Author: Makarius
c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	3
c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	4	ML heap operations.
c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	5	*)
c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	6
c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	7	signature ML_HEAP =
c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	8	sig
c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	9	val share_common_data: unit -> unit
c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	10	end;
c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	11
c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	12	structure ML_Heap: ML_HEAP =
c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	13	struct
c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	14	fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	15	end;