# HG changeset patch
# User wenzelm
# Date 1186151297 -7200
# Node ID bd3fc8ff6bc96ed92bd5199dbfba3e84c099760d
# Parent  8d789639814754c43eee7f05143c2bf99c26f4de
updated;

diff -r 8d7896398147 -r bd3fc8ff6bc9 doc-src/IsarImplementation/Thy/document/prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/prelim.tex	Fri Aug 03 16:28:15 2007 +0200
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex	Fri Aug 03 16:28:17 2007 +0200
@@ -181,8 +181,8 @@
   \end{mldecls}
   \begin{mldecls}
   \indexmltype{theory-ref}\verb|type theory_ref| \\
-  \indexml{Theory.self-ref}\verb|Theory.self_ref: theory -> theory_ref| \\
   \indexml{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\
+  \indexml{Theory.check-thy}\verb|Theory.check_thy: theory -> theory_ref| \\
   \end{mldecls}
 
   \begin{description}
@@ -211,8 +211,10 @@
   always valid theory; updates on the original are propagated
   automatically.
 
-  \item \verb|Theory.self_ref|~\isa{thy} and \verb|Theory.deref|~\isa{thy{\isacharunderscore}ref} convert between \verb|theory| and \verb|theory_ref|.  As the referenced theory
-  evolves monotonically over time, later invocations of \verb|Theory.deref| may refer to a larger context.
+  \item \verb|Theory.deref|~\isa{thy{\isacharunderscore}ref} turns a \verb|theory_ref| into an \verb|theory| value.  As the referenced
+  theory evolves monotonically over time, later invocations of \verb|Theory.deref| may refer to a larger context.
+
+  \item \verb|Theory.check_thy|~\isa{thy} produces a \verb|theory_ref| from a valid \verb|theory| value.
 
   \end{description}%
 \end{isamarkuptext}%
diff -r 8d7896398147 -r bd3fc8ff6bc9 src/Tools/Metis/metis.ML
--- a/src/Tools/Metis/metis.ML	Fri Aug 03 16:28:15 2007 +0200
+++ b/src/Tools/Metis/metis.ML	Fri Aug 03 16:28:17 2007 +0200
@@ -5386,7 +5386,7 @@
     | range NONE (SOME j) = "{n IN Z | n <= " ^ Int.toString j ^ "}"
     | range (SOME i) (SOME j) =
     "{n IN Z | " ^ Int.toString i ^ " <= n <= " ^ Int.toString j ^ "}";
-  fun oLeq (SOME (x:int)) (SOME y) = x <= y | oLeq _ _ = true;
+  fun oLeq (SOME (x: int)) (SOME y) = x <= y | oLeq _ _ = true;
   fun argToInt arg omin omax x =
     (case Int.fromString x of
        SOME i =>