--- a/src/Pure/Tools/nbe.ML Thu Sep 21 19:06:03 2006 +0200
+++ b/src/Pure/Tools/nbe.ML Thu Sep 21 19:06:16 2006 +0200
@@ -130,10 +130,10 @@
fun normalization_conv ct =
let val {sign, t, ...} = rep_cterm ct
- in Thm.invoke_oracle_i sign "Pure.Normalization" (sign, Normalization t) end;
+ in Thm.invoke_oracle_i sign "Pure.normalization" (sign, Normalization t) end;
val _ = Context.add_setup
- (Theory.add_oracle ("Normalization", normalization_oracle));
+ (Theory.add_oracle ("normalization", normalization_oracle));
(* Isar setup *)