src/Pure/ProofGeneral/proof_general_pgip.ML

 
         val thy_name = Path.implode o #1 o Path.split_ext o Path.base
 
         fun filerefs f =
             let val thy = thy_name f
-                val filerefs = map #1 (#uses (Thy_Load.check_thy [] (Path.dir f) thy))
+                val filerefs = map #1 (#uses (Thy_Load.check_thy (Path.dir f) thy))
             in
                 issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile,
                                      name=NONE, idtables=[], fileurls=filerefs})
             end
 
         fun thyrefs thy =
-            let val thyrefs = #imports (Thy_Load.check_thy [] Path.current thy)
+            let val thyrefs = #imports (Thy_Load.check_thy Path.current thy)
             in
                 issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
                                      name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,
                                                            ids=thyrefs}], fileurls=[]})
             end