src/Tools/nbe.ML
changeset 24166 7b28dc69bdbb
parent 24155 d86867645f4f
child 24219 e558fe311376
     1.1 --- a/src/Tools/nbe.ML	Tue Aug 07 09:38:48 2007 +0200
     1.2 +++ b/src/Tools/nbe.ML	Tue Aug 07 09:40:34 2007 +0200
     1.3 @@ -351,7 +351,8 @@
     1.4    Logic.mk_equals (t, eval thy code t t');
     1.5  
     1.6  fun normalization_invoke thy code t t' =
     1.7 -  Thm.invoke_oracle_i thy "Nbe.normalization" (thy, Normalization (code, t, t'));
     1.8 +  Thm.invoke_oracle_i thy "HOL.normalization" (thy, Normalization (code, t, t'));
     1.9 +  (*FIXME get rid of hardwired theory name "HOL"*)
    1.10  
    1.11  fun normalization_conv ct =
    1.12    let