src/Pure/thm.ML
changeset 28965 1de908189869
parent 28874 883ec8ee5e6e
child 28981 c9cf71e161b9
child 28991 694227dd3e8c
     1.1 --- a/src/Pure/thm.ML	Wed Dec 03 21:00:39 2008 -0800
     1.2 +++ b/src/Pure/thm.ML	Thu Dec 04 14:43:33 2008 +0100
     1.3 @@ -1732,9 +1732,9 @@
     1.4  fun add_oracle (bname, oracle) thy =
     1.5    let
     1.6      val naming = Sign.naming_of thy;
     1.7 -    val name = NameSpace.full naming bname;
     1.8 +    val name = NameSpace.full_name naming (Binding.name bname);
     1.9      val thy' = thy |> Oracles.map (fn (space, tab) =>
    1.10 -      (NameSpace.declare naming name space,
    1.11 +      (NameSpace.declare_base naming name space,
    1.12          Symtab.update_new (name, stamp ()) tab handle Symtab.DUP dup => err_dup_ora dup));
    1.13    in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;
    1.14