src/Pure/pure_setup.ML

   Theory.end_theory));
 structure Pure = struct val thy = ML_Context.the_global_context () end;
 Context.set_thread_data NONE;
 ThyInfo.register_theory Pure.thy;
 
-use_thy "CPure";
-structure CPure = struct val thy = theory "CPure" end;
-
 
 (* ML toplevel pretty printing *)
 
 install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);
 install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm);