# HG changeset patch
# User wenzelm
# Date 1186151295 -7200
# Node ID 8d789639814754c43eee7f05143c2bf99c26f4de
# Parent  0c6c943d8f1e92fa60664c65306b7f20b3c999c3
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;

diff -r 0c6c943d8f1e -r 8d7896398147 doc-src/IsarImplementation/Thy/prelim.thy
--- 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}
 *}
 
diff -r 0c6c943d8f1e -r 8d7896398147 src/HOL/OrderedGroup.thy
--- 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"]);
 
diff -r 0c6c943d8f1e -r 8d7896398147 src/HOL/Tools/datatype_codegen.ML
--- 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
diff -r 0c6c943d8f1e -r 8d7896398147 src/HOL/Tools/res_axioms.ML
--- 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.*)
diff -r 0c6c943d8f1e -r 8d7896398147 src/Pure/Isar/element.ML
--- 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),
diff -r 0c6c943d8f1e -r 8d7896398147 src/Pure/Tools/codegen_data.ML
--- 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, [])
diff -r 0c6c943d8f1e -r 8d7896398147 src/Pure/pure_thy.ML
--- 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*)
diff -r 0c6c943d8f1e -r 8d7896398147 src/Pure/theory.ML
--- 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;
diff -r 0c6c943d8f1e -r 8d7896398147 src/Tools/Compute_Oracle/compute.ML
--- 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
diff -r 0c6c943d8f1e -r 8d7896398147 src/Tools/Compute_Oracle/linker.ML
--- 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