diff -r 605f664d5115 -r 7b28dc69bdbb src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Tue Aug 07 09:38:48 2007 +0200
+++ b/src/Tools/nbe.ML	Tue Aug 07 09:40:34 2007 +0200
@@ -351,7 +351,8 @@
   Logic.mk_equals (t, eval thy code t t');
 
 fun normalization_invoke thy code t t' =
-  Thm.invoke_oracle_i thy "Nbe.normalization" (thy, Normalization (code, t, t'));
+  Thm.invoke_oracle_i thy "HOL.normalization" (thy, Normalization (code, t, t'));
+  (*FIXME get rid of hardwired theory name "HOL"*)
 
 fun normalization_conv ct =
   let