src/Pure/ROOT.ML

 fun use_thys args =
   Runtime.toplevel_program (fn () => Thy_Info.use_thys (map (rpair Position.none) args));
 val use_thy = use_thys o single;
 
 Proofterm.proofs := 0;
+
+structure PolyML = struct structure IntInf = PolyML.IntInf end;