--- a/doc-src/IsarImplementation/Thy/prelim.thy Thu Aug 02 23:18:13 2007 +0200
+++ b/doc-src/IsarImplementation/Thy/prelim.thy Fri Aug 03 16:28:15 2007 +0200
@@ -156,8 +156,8 @@
\end{mldecls}
\begin{mldecls}
@{index_ML_type theory_ref} \\
- @{index_ML Theory.self_ref: "theory -> theory_ref"} \\
@{index_ML Theory.deref: "theory_ref -> theory"} \\
+ @{index_ML Theory.check_thy: "theory -> theory_ref"} \\
\end{mldecls}
\begin{description}
@@ -187,12 +187,14 @@
always valid theory; updates on the original are propagated
automatically.
- \item @{ML "Theory.self_ref"}~@{text "thy"} and @{ML
- "Theory.deref"}~@{text "thy_ref"} convert between @{ML_type
- "theory"} and @{ML_type "theory_ref"}. As the referenced theory
- evolves monotonically over time, later invocations of @{ML
+ \item @{ML "Theory.deref"}~@{text "thy_ref"} turns a @{ML_type
+ "theory_ref"} into an @{ML_type "theory"} value. As the referenced
+ theory evolves monotonically over time, later invocations of @{ML
"Theory.deref"} may refer to a larger context.
+ \item @{ML "Theory.check_thy"}~@{text "thy"} produces a @{ML_type
+ "theory_ref"} from a valid @{ML_type "theory"} value.
+
\end{description}
*}
--- a/src/HOL/OrderedGroup.thy Thu Aug 02 23:18:13 2007 +0200
+++ b/src/HOL/OrderedGroup.thy Fri Aug 03 16:28:15 2007 +0200
@@ -1104,7 +1104,7 @@
val eq_reflection = @{thm eq_reflection};
-val thy_ref = Theory.self_ref @{theory};
+val thy_ref = Theory.check_thy @{theory};
val T = TFree("'a", ["OrderedGroup.ab_group_add"]);
--- a/src/HOL/Tools/datatype_codegen.ML Thu Aug 02 23:18:13 2007 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML Fri Aug 03 16:28:15 2007 +0200
@@ -596,7 +596,7 @@
let
fun add_eq_thms (dtco, (_, (vs, cs))) thy =
let
- val thy_ref = Theory.self_ref thy;
+ val thy_ref = Theory.check_thy thy;
val const = ("op =", SOME dtco);
val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
in
--- a/src/HOL/Tools/res_axioms.ML Thu Aug 02 23:18:13 2007 +0200
+++ b/src/HOL/Tools/res_axioms.ML Fri Aug 03 16:28:15 2007 +0200
@@ -80,7 +80,7 @@
inside that theory -- because it's needed for Skolemization *)
(*This will refer to the final version of theory ATP_Linkup.*)
-val recon_thy_ref = Theory.self_ref (the_context ());
+val recon_thy_ref = Theory.check_thy @{theory}
(*If called while ATP_Linkup is being created, it will transfer to the
current version. If called afterward, it will transfer to the final version.*)
--- a/src/Pure/Isar/element.ML Thu Aug 02 23:18:13 2007 +0200
+++ b/src/Pure/Isar/element.ML Fri Aug 03 16:28:15 2007 +0200
@@ -411,7 +411,7 @@
in if null subst then th else th |> hyps_rule (instantiate_tfrees thy subst) end;
fun instT_morphism thy env =
- let val thy_ref = Theory.self_ref thy in
+ let val thy_ref = Theory.check_thy thy in
Morphism.morphism
{name = I, var = I,
typ = instT_type env,
@@ -460,7 +460,7 @@
end;
fun inst_morphism thy envs =
- let val thy_ref = Theory.self_ref thy in
+ let val thy_ref = Theory.check_thy thy in
Morphism.morphism
{name = I, var = I,
typ = instT_type (#1 envs),
--- a/src/Pure/Tools/codegen_data.ML Thu Aug 02 23:18:13 2007 +0200
+++ b/src/Pure/Tools/codegen_data.ML Fri Aug 03 16:28:15 2007 +0200
@@ -100,7 +100,7 @@
case Susp.peek r
of SOME thms => (Susp.value o f thy) thms
| NONE => let
- val thy_ref = Theory.self_ref thy;
+ val thy_ref = Theory.check_thy thy;
in lazy_thms (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end;
fun merge' _ ([], []) = (false, [])
--- a/src/Pure/pure_thy.ML Thu Aug 02 23:18:13 2007 +0200
+++ b/src/Pure/pure_thy.ML Fri Aug 03 16:28:15 2007 +0200
@@ -238,8 +238,8 @@
fun lookup_thms thy =
let
- val thy_ref = Theory.self_ref thy;
val (space, thms) = #theorems (get_theorems thy);
+ val thy_ref = Theory.check_thy thy;
in
fn name =>
Option.map (map (Thm.transfer (Theory.deref thy_ref))) (*dynamic identity*)
--- a/src/Pure/theory.ML Thu Aug 02 23:18:13 2007 +0200
+++ b/src/Pure/theory.ML Fri Aug 03 16:28:15 2007 +0200
@@ -32,7 +32,7 @@
val axioms_of: theory -> (string * term) list
val all_axioms_of: theory -> (string * term) list
val defs_of : theory -> Defs.T
- val self_ref: theory -> theory_ref
+ val check_thy: theory -> theory_ref
val deref: theory_ref -> theory
val merge: theory * theory -> theory
val merge_refs: theory_ref * theory_ref -> theory_ref
@@ -65,7 +65,7 @@
val parents_of = Context.parents_of;
val ancestors_of = Context.ancestors_of;
-val self_ref = Context.self_ref;
+val check_thy = Context.check_thy;
val deref = Context.deref;
val merge = Context.merge;
val merge_refs = Context.merge_refs;
--- a/src/Tools/Compute_Oracle/compute.ML Thu Aug 02 23:18:13 2007 +0200
+++ b/src/Tools/Compute_Oracle/compute.ML Fri Aug 03 16:28:15 2007 +0200
@@ -267,7 +267,7 @@
val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable
- in Computer (Theory.self_ref thy, encoding, Termtab.keys hyptable, shyptable, prog) end
+ in Computer (Theory.check_thy thy, encoding, Termtab.keys hyptable, shyptable, prog) end
(*fun timeit f =
let
--- a/src/Tools/Compute_Oracle/linker.ML Thu Aug 02 23:18:13 2007 +0200
+++ b/src/Tools/Compute_Oracle/linker.ML Fri Aug 03 16:28:15 2007 +0200
@@ -365,8 +365,9 @@
end)
ths (cs, [])
val (_, ths) = add_monos thy monocs ths
+ val computer = create_computer machine thy ths
in
- PComputer (machine, Theory.self_ref thy, ref (create_computer machine thy ths), ref ths)
+ PComputer (machine, Theory.check_thy thy, ref computer, ref ths)
end
fun add_instances (PComputer (machine, thyref, rcomputer, rths)) cs =
@@ -389,4 +390,4 @@
map (fn ct => Compute.rewrite (!rcomputer) ct) cts
end
-end
\ No newline at end of file
+end