src/Pure/ML/ml_pervasive1.ML
author wenzelm
Thu Apr 07 16:53:43 2016 +0200 (2016-04-07)
changeset 62902 3c0f53eae166
parent 62889 99c7f31615c2
child 62923 3a122e1e352a
permissions -rw-r--r--
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
avoid slowdown of Resources.loaded_files due to command name 'use' in Pure base syntax;
     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.put_generic_context NONE;
    15 
    16 val use = ML_file;