src/Pure/ML/ml_pervasive1.ML
author wenzelm
Wed Apr 06 11:57:21 2016 +0200 (2016-04-06)
changeset 62886 72c475e03e22
parent 62884 66494de0aafe
child 62889 99c7f31615c2
permissions -rw-r--r--
simplified bootstrap: critical structures remain accessible in ML_Root context;
     1 (*  Title:      Pure/ML/ml_pervasive1.ML
     2     Author:     Makarius
     3 
     4 Pervasive ML environment: final setup.
     5 *)
     6 
     7 List.app ML_Name_Space.forget_structure
     8   (remove (op =) "PolyML" ML_Name_Space.bootstrap_structures);
     9 
    10 structure PolyML = struct structure IntInf = PolyML.IntInf end;
    11 
    12 Proofterm.proofs := 0;
    13 
    14 Context.set_thread_data NONE;