src/Pure/pure_setup.ML
changeset 26608 ff838a61dad6
parent 26463 9283b4185fdf
child 26957 e3f04fdd994d
equal deleted inserted replaced
26607:e36d16985402 26608:ff838a61dad6
    13 fun time_use name     = Toplevel.program (fn () => ThyInfo.time_use name);
    13 fun time_use name     = Toplevel.program (fn () => ThyInfo.time_use name);
    14 fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name);
    14 fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name);
    15 
    15 
    16 
    16 
    17 (* the Pure theories *)
    17 (* the Pure theories *)
       
    18 
       
    19 val theory = ThyInfo.get_theory;
    18 
    20 
    19 Context.>> (Context.map_theory
    21 Context.>> (Context.map_theory
    20  (OuterSyntax.process_file (Path.explode "Pure.thy") #>
    22  (OuterSyntax.process_file (Path.explode "Pure.thy") #>
    21   Theory.end_theory));
    23   Theory.end_theory));
    22 structure Pure = struct val thy = ML_Context.the_global_context () end;
    24 structure Pure = struct val thy = ML_Context.the_global_context () end;