src/Tools/Compute_Oracle/linker.ML

     end
 
 fun substs_of (Instances (_,_,_,substs)) = Substtab.keys substs
 
 local
-    fun get_thm thmname = PureThy.get_thm (theory "Main") (Name thmname)
+    fun get_thm thmname = PureThy.get_thm (theory "Main") (Facts.Named (thmname, NONE))
     val eq_th = get_thm "HOL.eq_reflection"
 in
-  fun eq_to_meta th = (eq_th OF [th] handle _ => th)
+  fun eq_to_meta th = (eq_th OF [th] handle THM _ => th)
 end
 
 
 local