src/Tools/Compute_Oracle/linker.ML
changeset 37869 e9c6a7fe1989
parent 37863 7f113caabcf4
--- a/src/Tools/Compute_Oracle/linker.ML	Wed Jul 21 15:02:51 2010 +0200
+++ b/src/Tools/Compute_Oracle/linker.ML	Wed Jul 21 15:13:36 2010 +0200
@@ -190,12 +190,7 @@
 
 fun substs_of (Instances (_,_,_,substs)) = Substtab.keys substs
 
-local
-    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)
-end
+fun eq_to_meta th = (@{thm HOL.eq_reflection} OF [th] handle THM _ => th)
 
 
 local