# HG changeset patch
# User wenzelm
# Date 1236278882 -3600
# Node ID a32700e45ab30ec6d4d805d52e3d1952f19abcc6
# Parent  39b931e00ba996c8737603d8562e979a4cce4e3c
Thm.add_oracle interface: replaced old bstring by binding;

diff -r 39b931e00ba9 -r a32700e45ab3 doc-src/IsarImplementation/Thy/Logic.thy
--- a/doc-src/IsarImplementation/Thy/Logic.thy	Thu Mar 05 18:19:20 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Logic.thy	Thu Mar 05 19:48:02 2009 +0100
@@ -556,7 +556,7 @@
   @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
   @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
   @{index_ML Thm.axiom: "theory -> string -> thm"} \\
-  @{index_ML Thm.add_oracle: "bstring * ('a -> cterm) -> theory
+  @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory
   -> (string * ('a -> thm)) * theory"} \\
   \end{mldecls}
   \begin{mldecls}
@@ -613,7 +613,7 @@
   \item @{ML Thm.axiom}~@{text "thy name"} retrieves a named
   axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
 
-  \item @{ML Thm.add_oracle}~@{text "(name, oracle)"} produces a named
+  \item @{ML Thm.add_oracle}~@{text "(binding, oracle)"} produces a named
   oracle rule, essentially generating arbitrary axioms on the fly,
   cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
 
diff -r 39b931e00ba9 -r a32700e45ab3 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Mar 05 18:19:20 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Mar 05 19:48:02 2009 +0100
@@ -150,10 +150,12 @@
     val oracle = SymbolPos.content (SymbolPos.explode (oracle_txt, pos));
     val txt =
       "local\n\
-      \  val name = " ^ quote name ^ ";\n\
+      \  val name = " ^ ML_Syntax.print_string name ^ ";\n\
+      \  val pos = " ^ ML_Syntax.print_position pos ^ ";\n\
+      \  val binding = Binding.make (name, pos);\n\
       \  val oracle = " ^ oracle ^ ";\n\
       \in\n\
-      \  val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (name, oracle))));\n\
+      \  val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, oracle))));\n\
       \end;\n";
   in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false pos txt)) end;
 
diff -r 39b931e00ba9 -r a32700e45ab3 src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Thu Mar 05 18:19:20 2009 +0100
+++ b/src/Pure/Isar/skip_proof.ML	Thu Mar 05 19:48:02 2009 +0100
@@ -20,7 +20,7 @@
 (* oracle setup *)
 
 val (_, skip_proof) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle ("skip_proof", fn (thy, prop) =>
+  (Thm.add_oracle (Binding.name "skip_proof", fn (thy, prop) =>
     if ! quick_and_dirty then Thm.cterm_of thy prop
     else error "Proof may be skipped in quick_and_dirty mode only!")));
 
diff -r 39b931e00ba9 -r a32700e45ab3 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Thu Mar 05 18:19:20 2009 +0100
+++ b/src/Pure/codegen.ML	Thu Mar 05 19:48:02 2009 +0100
@@ -938,7 +938,7 @@
   in e () end;
 
 val (_, evaluation_conv) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle ("evaluation", fn ct =>
+  (Thm.add_oracle (Binding.name "evaluation", fn ct =>
     let
       val thy = Thm.theory_of_cterm ct;
       val t = Thm.term_of ct;
diff -r 39b931e00ba9 -r a32700e45ab3 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Mar 05 18:19:20 2009 +0100
+++ b/src/Pure/thm.ML	Thu Mar 05 19:48:02 2009 +0100
@@ -151,7 +151,7 @@
   val proof_of: thm -> proof
   val join_proof: thm -> unit
   val extern_oracles: theory -> xstring list
-  val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
+  val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
 end;
 
 structure Thm:> THM =
@@ -1698,7 +1698,7 @@
 
 structure Oracles = TheoryDataFun
 (
-  type T = stamp NameSpace.table;
+  type T = serial NameSpace.table;
   val empty = NameSpace.empty_table;
   val copy = I;
   val extend = I;
@@ -1708,13 +1708,12 @@
 
 val extern_oracles = map #1 o NameSpace.extern_table o Oracles.get;
 
-fun add_oracle (bname, oracle) thy =
+fun add_oracle (b, oracle) thy =
   let
     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 naming (Binding.name bname) space |> snd,
-        Symtab.update_new (name, stamp ()) tab handle Symtab.DUP dup => err_dup_ora dup));
+    val (name, tab') = NameSpace.bind naming (b, serial ()) (Oracles.get thy)
+      handle Symtab.DUP _ => err_dup_ora (Binding.str_of b);
+    val thy' = Oracles.put tab' thy;
   in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;
 
 end;
diff -r 39b931e00ba9 -r a32700e45ab3 src/Tools/Compute_Oracle/compute.ML
--- a/src/Tools/Compute_Oracle/compute.ML	Thu Mar 05 18:19:20 2009 +0100
+++ b/src/Tools/Compute_Oracle/compute.ML	Thu Mar 05 19:48:02 2009 +0100
@@ -371,7 +371,7 @@
 fun merge_shyps shyps1 shyps2 = Sorttab.keys (add_shyps shyps2 (add_shyps shyps1 Sorttab.empty))
 
 val (_, export_oracle) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle ("compute", fn (thy, hyps, shyps, prop) =>
+  (Thm.add_oracle (Binding.name "compute", fn (thy, hyps, shyps, prop) =>
     let
         val shyptab = add_shyps shyps Sorttab.empty
         fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab
diff -r 39b931e00ba9 -r a32700e45ab3 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Thu Mar 05 18:19:20 2009 +0100
+++ b/src/Tools/nbe.ML	Thu Mar 05 19:48:02 2009 +0100
@@ -466,7 +466,7 @@
 (* evaluation oracle *)
 
 val (_, norm_oracle) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle ("norm", fn (thy, t, naming, program, vs_ty_t, deps) =>
+  (Thm.add_oracle (Binding.name "norm", fn (thy, t, naming, program, vs_ty_t, deps) =>
     Thm.cterm_of thy (Logic.mk_equals (t, eval thy t naming program vs_ty_t deps)))));
 
 fun add_triv_classes thy =