# HG changeset patch
# User wenzelm
# Date 1158858376 -7200
# Node ID 5ce43b38a1759519f1c65e67a8de7b0d63db7b91
# Parent  21e096f30c5d52116352acc7506a0d9a39f076c4
tuned oracle name;

diff -r 21e096f30c5d -r 5ce43b38a175 src/Pure/Tools/nbe.ML
--- 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 *)