# HG changeset patch
# User wenzelm
# Date 1279718016 -7200
# Node ID e9c6a7fe1989b03daba9ab8b761f1ba76767aa7a
# Parent  59eed00bfd8e01e2bc614a2052cbd222f35ee828
explicit dependency on theory HOL;

diff -r 59eed00bfd8e -r e9c6a7fe1989 src/Tools/Compute_Oracle/Compute_Oracle.thy
--- 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
 
diff -r 59eed00bfd8e -r e9c6a7fe1989 src/Tools/Compute_Oracle/linker.ML
--- 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