src/Pure/ML/ml_pervasive1.ML
author wenzelm
Wed Apr 06 16:33:33 2016 +0200 (2016-04-06)
changeset 62889 99c7f31615c2
parent 62886 72c475e03e22
child 62902 3c0f53eae166
permissions -rw-r--r--
clarified modules;
tuned signature;
wenzelm@62883
     1
(*  Title:      Pure/ML/ml_pervasive1.ML
wenzelm@62846
     2
    Author:     Makarius
wenzelm@62846
     3
wenzelm@62852
     4
Pervasive ML environment: final setup.
wenzelm@62846
     5
*)
wenzelm@62846
     6
wenzelm@62886
     7
List.app ML_Name_Space.forget_structure
wenzelm@62886
     8
  (remove (op =) "PolyML" ML_Name_Space.bootstrap_structures);
wenzelm@62886
     9
wenzelm@62886
    10
structure PolyML = struct structure IntInf = PolyML.IntInf end;
wenzelm@62846
    11
wenzelm@62846
    12
Proofterm.proofs := 0;
wenzelm@62846
    13
wenzelm@62889
    14
Context.put_generic_context NONE;