--- a/src/Pure/thm.ML Thu Dec 04 18:37:46 2008 -0800
+++ b/src/Pure/thm.ML Fri Dec 05 08:05:14 2008 +0100
@@ -1703,7 +1703,7 @@
val naming = Sign.naming_of thy;
val name = NameSpace.full_name naming (Binding.name bname);
val thy' = thy |> Oracles.map (fn (space, tab) =>
- (NameSpace.declare_base naming name space,
+ (NameSpace.declare naming (Binding.name bname) space |> snd,
Symtab.update_new (name, stamp ()) tab handle Symtab.DUP dup => err_dup_ora dup));
in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;