src/Pure/thm.ML
changeset 30466 5f31e24937c5
parent 30342 d32daa6aba3c
child 30554 73f8bd5f0af8
     1.1 --- a/src/Pure/thm.ML	Thu Mar 12 11:09:26 2009 +0100
     1.2 +++ b/src/Pure/thm.ML	Thu Mar 12 11:10:02 2009 +0100
     1.3 @@ -1700,7 +1700,7 @@
     1.4  fun add_oracle (b, oracle) thy =
     1.5    let
     1.6      val naming = Sign.naming_of thy;
     1.7 -    val (name, tab') = NameSpace.bind naming (b, serial ()) (Oracles.get thy)
     1.8 +    val (name, tab') = NameSpace.define naming (b, serial ()) (Oracles.get thy)
     1.9        handle Symtab.DUP _ => err_dup_ora (Binding.str_of b);
    1.10      val thy' = Oracles.put tab' thy;
    1.11    in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;