src/Tools/Compute_Oracle/linker.ML

--- a/src/Tools/Compute_Oracle/linker.ML	Wed Mar 19 22:50:42 2008 +0100
+++ b/src/Tools/Compute_Oracle/linker.ML	Thu Mar 20 00:20:44 2008 +0100
@@ -192,7 +192,7 @@
 fun substs_of (Instances (_,_,_,substs)) = Substtab.keys substs
 
 local
-    fun get_thm thmname = PureThy.get_thm (theory "Main") (Facts.Named (thmname, NONE))
+    fun get_thm thmname = PureThy.get_thm (theory "Main") thmname
     val eq_th = get_thm "HOL.eq_reflection"
 in
   fun eq_to_meta th = (eq_th OF [th] handle THM _ => th)