| changeset 24166 | 7b28dc69bdbb |
| parent 24155 | d86867645f4f |
| child 24219 | e558fe311376 |
--- 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