--- 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}.
--- 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;
--- 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!")));
--- 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;
--- 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;
--- 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
--- 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 =