explicit dependency on theory HOL;

--- a/src/Tools/Compute_Oracle/Compute_Oracle.thy	Wed Jul 21 15:02:51 2010 +0200
+++ b/src/Tools/Compute_Oracle/Compute_Oracle.thy	Wed Jul 21 15:13:36 2010 +0200
@@ -4,7 +4,7 @@
 Steven Obua's evaluator.
 *)
 
-theory Compute_Oracle imports Pure
+theory Compute_Oracle imports HOL
 uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "report.ML" "compute.ML" "linker.ML"
 begin
 

--- 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