src/Pure/thm.ML
changeset 28991 694227dd3e8c
parent 28965 1de908189869
child 28992 c4ae153d78ab
     1.1 --- a/src/Pure/thm.ML	Thu Dec 04 14:44:07 2008 +0100
     1.2 +++ b/src/Pure/thm.ML	Fri Dec 05 08:04:53 2008 +0100
     1.3 @@ -1734,7 +1734,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