src/Pure/thm.ML
changeset 28992 c4ae153d78ab
parent 28981 c9cf71e161b9
parent 28991 694227dd3e8c
child 28996 01918abaa9e7
     1.1 --- a/src/Pure/thm.ML	Thu Dec 04 18:37:46 2008 -0800
     1.2 +++ b/src/Pure/thm.ML	Fri Dec 05 08:05:14 2008 +0100
     1.3 @@ -1703,7 +1703,7 @@
     1.4      val naming = Sign.naming_of thy;
     1.5      val name = NameSpace.full_name naming (Binding.name bname);
     1.6      val thy' = thy |> Oracles.map (fn (space, tab) =>
     1.7 -      (NameSpace.declare_base naming name space,
     1.8 +      (NameSpace.declare naming (Binding.name bname) space |> snd,
     1.9          Symtab.update_new (name, stamp ()) tab handle Symtab.DUP dup => err_dup_ora dup));
    1.10    in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;
    1.11