isabelle: src/Pure/ML/ml_pervasive1.ML@66494de0aafe (annotated)

62883 b04e9fe29223 clarified ML bootstrap; wenzelm parents: 62875 diff changeset	1	(* Title: Pure/ML/ml_pervasive1.ML
62846 3c576c7f9731 clarified final setup of ML environment; wenzelm parents: diff changeset	2	Author: Makarius
3c576c7f9731 clarified final setup of ML environment; wenzelm parents: diff changeset	3
62852 dd5f3a6fee73 clarified modules; wenzelm parents: 62851 diff changeset	4	Pervasive ML environment: final setup.
62846 3c576c7f9731 clarified final setup of ML environment; wenzelm parents: diff changeset	5	*)
3c576c7f9731 clarified final setup of ML environment; wenzelm parents: diff changeset	6
62875 5a0c06491974 clarified bootstrap environment; wenzelm parents: 62872 diff changeset	7	if Options.default_bool "ML_system_bootstrap" then ()
62851 07eea2843b82 option ML_system_unsafe; wenzelm parents: 62847 diff changeset	8	else
62875 5a0c06491974 clarified bootstrap environment; wenzelm parents: 62872 diff changeset	9	(List.app ML_Name_Space.forget_structure
5a0c06491974 clarified bootstrap environment; wenzelm parents: 62872 diff changeset	10	(remove (op =) "PolyML" ML_Name_Space.bootstrap_structures);
5a0c06491974 clarified bootstrap environment; wenzelm parents: 62872 diff changeset	11	ML \<open>structure PolyML = struct structure IntInf = PolyML.IntInf end\<close>);
62846 3c576c7f9731 clarified final setup of ML environment; wenzelm parents: diff changeset	12
3c576c7f9731 clarified final setup of ML environment; wenzelm parents: diff changeset	13	Proofterm.proofs := 0;
3c576c7f9731 clarified final setup of ML environment; wenzelm parents: diff changeset	14
3c576c7f9731 clarified final setup of ML environment; wenzelm parents: diff changeset	15	Context.set_thread_data NONE;

author	wenzelm
	Wed, 06 Apr 2016 11:44:34 +0200
changeset 62884	66494de0aafe
parent 62883	b04e9fe29223
child 62886	72c475e03e22
permissions	-rw-r--r--