# HG changeset patch
# User wenzelm
# Date 1318237929 -7200
# Node ID d78ec6c10fa13b7f0c61a5080c76b4b3ee5ac75f
# Parent  49e305100097056b94d4383fc04b7cc42584f496# Parent  414b083058e403182dda111974d365e343b69480
merged

diff -r 49e305100097 -r d78ec6c10fa1 .hgtags
--- a/.hgtags	Sun Oct 09 11:13:53 2011 +0200
+++ b/.hgtags	Mon Oct 10 11:12:09 2011 +0200
@@ -27,3 +27,5 @@
 6a973bd4394996c31f638e5c59ea6bb953335c9a Isabelle2009-1
 35815ce9218a8822a50f5d80b96aa8d1970ec35d Isabelle2009-2
 6d736d983d5cfec4a6c6fba174db2cd93493a96b Isabelle2011
+76fef3e570043b84a32716b5633085d2fb215525 Isabelle2011-1
+
diff -r 49e305100097 -r d78ec6c10fa1 Admin/CHECKLIST
--- a/Admin/CHECKLIST	Sun Oct 09 11:13:53 2011 +0200
+++ b/Admin/CHECKLIST	Mon Oct 10 11:12:09 2011 +0200
@@ -42,12 +42,12 @@
 
 - makebin (multiplatform);
 
-- makebin -l on fast machine;
-
 - makebundle (multiplatform);
 
 - hdiutil create -srcfolder DIR DMG (Mac OS);
 
+- makebin -l on fast machine, based on renamed bundle with deleted heaps;
+
 
 Final release stage
 ===================
diff -r 49e305100097 -r d78ec6c10fa1 Admin/MacOS/App1/script
--- a/Admin/MacOS/App1/script	Sun Oct 09 11:13:53 2011 +0200
+++ b/Admin/MacOS/App1/script	Mon Oct 10 11:12:09 2011 +0200
@@ -106,8 +106,7 @@
   ( "$ISABELLE_TOOL" emacs "${EMACS_OPTIONS[@]}" "$@" ) > "$OUTPUT" 2>&1
   RC=$?
 else
-  rm -f "$OUTPUT" && touch "$OUTPUT"
-  "$ISABELLE_TOOL" jedit "$@"
+  ( "$ISABELLE_TOOL" jedit "$@" ) > "$OUTPUT" 2>&1
   RC=$?
 fi
 
diff -r 49e305100097 -r d78ec6c10fa1 Admin/build
--- a/Admin/build	Sun Oct 09 11:13:53 2011 +0200
+++ b/Admin/build	Mon Oct 10 11:12:09 2011 +0200
@@ -84,7 +84,7 @@
 
 function build_jars ()
 {
-  "$ISABELLE_HOME/lib/scripts/java_ext_dirs" >/dev/null
+  "$ISABELLE_TOOL" env "$ISABELLE_HOME/lib/scripts/java_ext_dirs" >/dev/null
   pushd "$ISABELLE_HOME/src/Pure" >/dev/null
   "$ISABELLE_TOOL" env ./build-jars "$@" || exit $?
   popd >/dev/null
diff -r 49e305100097 -r d78ec6c10fa1 Admin/makedist
--- a/Admin/makedist	Sun Oct 09 11:13:53 2011 +0200
+++ b/Admin/makedist	Mon Oct 10 11:12:09 2011 +0200
@@ -178,7 +178,6 @@
     echo
   } >ANNOUNCE
 else
-  rm Isabelle Isabelle.exe
   perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML
 fi
 
diff -r 49e305100097 -r d78ec6c10fa1 doc-src/IsarRef/Thy/First_Order_Logic.thy
--- a/doc-src/IsarRef/Thy/First_Order_Logic.thy	Sun Oct 09 11:13:53 2011 +0200
+++ b/doc-src/IsarRef/Thy/First_Order_Logic.thy	Mon Oct 10 11:12:09 2011 +0200
@@ -47,7 +47,7 @@
 text {*
   \noindent Substitution is very powerful, but also hard to control in
   full generality.  We derive some common symmetry~/ transitivity
-  schemes of as particular consequences.
+  schemes of @{term equal} as particular consequences.
 *}
 
 theorem sym [sym]:
diff -r 49e305100097 -r d78ec6c10fa1 doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Sun Oct 09 11:13:53 2011 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy	Mon Oct 10 11:12:09 2011 +0200
@@ -129,7 +129,7 @@
   proof structure at all, but goes back right to the theory level.
   Furthermore, @{command "oops"} does not produce any result theorem
   --- there is no intended claim to be able to complete the proof
-  anyhow.
+  in any way.
 
   A typical application of @{command "oops"} is to explain Isar proofs
   \emph{within} the system itself, in conjunction with the document
diff -r 49e305100097 -r d78ec6c10fa1 doc-src/IsarRef/Thy/Synopsis.thy
--- a/doc-src/IsarRef/Thy/Synopsis.thy	Sun Oct 09 11:13:53 2011 +0200
+++ b/doc-src/IsarRef/Thy/Synopsis.thy	Mon Oct 10 11:12:09 2011 +0200
@@ -907,7 +907,7 @@
 
 text {* There is nothing special about logical connectives (@{text
   "\<and>"}, @{text "\<or>"}, @{text "\<forall>"}, @{text "\<exists>"} etc.).  Operators from
-  set-theory or lattice-theory for analogously.  It is only a matter
+  set-theory or lattice-theory work analogously.  It is only a matter
   of rule declarations in the library; rules can be also specified
   explicitly.
 *}
@@ -1105,4 +1105,4 @@
   note `C`
 end
 
-end
\ No newline at end of file
+end
diff -r 49e305100097 -r d78ec6c10fa1 doc-src/IsarRef/Thy/document/First_Order_Logic.tex
--- a/doc-src/IsarRef/Thy/document/First_Order_Logic.tex	Sun Oct 09 11:13:53 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/First_Order_Logic.tex	Mon Oct 10 11:12:09 2011 +0200
@@ -68,7 +68,7 @@
 \begin{isamarkuptext}%
 \noindent Substitution is very powerful, but also hard to control in
   full generality.  We derive some common symmetry~/ transitivity
-  schemes of as particular consequences.%
+  schemes of \isa{equal} as particular consequences.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{theorem}\isamarkupfalse%
diff -r 49e305100097 -r d78ec6c10fa1 doc-src/IsarRef/Thy/document/Proof.tex
--- a/doc-src/IsarRef/Thy/document/Proof.tex	Sun Oct 09 11:13:53 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex	Mon Oct 10 11:12:09 2011 +0200
@@ -159,7 +159,7 @@
   proof structure at all, but goes back right to the theory level.
   Furthermore, \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} does not produce any result theorem
   --- there is no intended claim to be able to complete the proof
-  anyhow.
+  in any way.
 
   A typical application of \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} is to explain Isar proofs
   \emph{within} the system itself, in conjunction with the document
diff -r 49e305100097 -r d78ec6c10fa1 doc-src/IsarRef/Thy/document/Synopsis.tex
--- a/doc-src/IsarRef/Thy/document/Synopsis.tex	Sun Oct 09 11:13:53 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Synopsis.tex	Mon Oct 10 11:12:09 2011 +0200
@@ -2258,7 +2258,7 @@
 %
 \begin{isamarkuptext}%
 There is nothing special about logical connectives (\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616E643E}{\isasymand}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6F723E}{\isasymor}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}{\isaliteral{22}{\isachardoublequote}}} etc.).  Operators from
-  set-theory or lattice-theory for analogously.  It is only a matter
+  set-theory or lattice-theory work analogously.  It is only a matter
   of rule declarations in the library; rules can be also specified
   explicitly.%
 \end{isamarkuptext}%
@@ -2708,6 +2708,7 @@
 {\isafoldtheory}%
 %
 \isadelimtheory
+\isanewline
 %
 \endisadelimtheory
 \end{isabellebody}%
diff -r 49e305100097 -r d78ec6c10fa1 doc-src/TutorialI/Documents/Documents.thy
--- a/doc-src/TutorialI/Documents/Documents.thy	Sun Oct 09 11:13:53 2011 +0200
+++ b/doc-src/TutorialI/Documents/Documents.thy	Mon Oct 10 11:12:09 2011 +0200
@@ -344,7 +344,7 @@
   session is derived from a single parent, usually an object-logic
   image like \texttt{HOL}.  This results in an overall tree structure,
   which is reflected by the output location in the file system
-  (usually rooted at \verb,~/.isabelle/browser_info,).
+  (usually rooted at \verb,~/.isabelle/IsabelleXXXX/browser_info,).
 
   \medskip The easiest way to manage Isabelle sessions is via
   \texttt{isabelle mkdir} (generates an initial session source setup)
diff -r 49e305100097 -r d78ec6c10fa1 doc-src/TutorialI/Documents/document/Documents.tex
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Sun Oct 09 11:13:53 2011 +0200
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Mon Oct 10 11:12:09 2011 +0200
@@ -417,7 +417,7 @@
   session is derived from a single parent, usually an object-logic
   image like \texttt{HOL}.  This results in an overall tree structure,
   which is reflected by the output location in the file system
-  (usually rooted at \verb,~/.isabelle/browser_info,).
+  (usually rooted at \verb,~/.isabelle/IsabelleXXXX/browser_info,).
 
   \medskip The easiest way to manage Isabelle sessions is via
   \texttt{isabelle mkdir} (generates an initial session source setup)
diff -r 49e305100097 -r d78ec6c10fa1 etc/user-settings.sample
--- a/etc/user-settings.sample	Sun Oct 09 11:13:53 2011 +0200
+++ b/etc/user-settings.sample	Mon Oct 10 11:12:09 2011 +0200
@@ -1,6 +1,6 @@
 # -*- shell-script -*- :mode=shellscript:
 #
-# Isabelle user settings sample -- for use in ~/.isabelle/etc/settings
+# Isabelle user settings sample -- for use in $ISABELLE_HOME_USER/etc/settings
 
 ISABELLE_USEDIR_OPTIONS="-i true -d pdf"
 ISABELLE_LOGIC=HOL
diff -r 49e305100097 -r d78ec6c10fa1 lib/Tools/java
--- a/lib/Tools/java	Sun Oct 09 11:13:53 2011 +0200
+++ b/lib/Tools/java	Mon Oct 10 11:12:09 2011 +0200
@@ -8,6 +8,13 @@
 
 JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
 
+if "$JAVA_EXE" -version >/dev/null 2>/dev/null; then
+  :
+else
+  echo "Bad Java executable: \"$JAVA_EXE\"" >&2
+  exit 2
+fi
+
 if "$JAVA_EXE" -server >/dev/null 2>/dev/null; then
   SERVER="-server"
 else
diff -r 49e305100097 -r d78ec6c10fa1 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Sun Oct 09 11:13:53 2011 +0200
+++ b/lib/scripts/getsettings	Mon Oct 10 11:12:09 2011 +0200
@@ -14,7 +14,7 @@
 export ISABELLE_HOME
 if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; }
 then
-  echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems later on!"
+  echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems!"
   echo 1>&2 "### ISABELLE_HOME=\"$ISABELLE_HOME\""
 fi
 
diff -r 49e305100097 -r d78ec6c10fa1 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sun Oct 09 11:13:53 2011 +0200
+++ b/src/Pure/System/isabelle_system.scala	Mon Oct 10 11:12:09 2011 +0200
@@ -110,6 +110,16 @@
   def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path))
   def platform_file(path: Path): File = new File(platform_path(path))
 
+  def platform_file_url(raw_path: Path): String =
+  {
+    val path = raw_path.expand
+    require(path.is_absolute)
+    val s = platform_path(path).replaceAll(" ", "%20")
+    if (!Platform.is_windows) "file://" + s
+    else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
+    else "file:///" + s.replace('\\', '/')
+  }
+
   def posix_path(jvm_path: String): String = standard_system.posix_path(jvm_path)
 
 
diff -r 49e305100097 -r d78ec6c10fa1 src/Tools/jEdit/PIDE.png
Binary file src/Tools/jEdit/PIDE.png has changed
diff -r 49e305100097 -r d78ec6c10fa1 src/Tools/jEdit/README.html
--- a/src/Tools/jEdit/README.html	Sun Oct 09 11:13:53 2011 +0200
+++ b/src/Tools/jEdit/README.html	Mon Oct 10 11:12:09 2011 +0200
@@ -7,17 +7,43 @@
 <style type="text/css" media="screen">
 body { font-family: STIXGeneral, IsabelleText; font-size: 14pt; }
 </style>
-<title>Notes on the Isabelle/jEdit Prover IDE</title>
+<title>Welcome to the Isabelle/jEdit Prover IDE</title>
 </head>
 
 <body>
 
-<h2>The Isabelle/jEdit Prover IDE (based on Isabelle/Scala)</h2>
+<center><h2><img alt="PIDE" src="PIDE.png" width="230" align="middle"/></h2></center>
+
+<p>
+  <b>PIDE</b> is a novel framework for sophisticated Prover IDEs,
+  based on Isabelle/Scala technology that is integrated with Isabelle.
+  It is build around a concept of
+  <em>asynchronous document processing</em>, which is supported
+  natively by the <em>parallel proof engine</em> implemented in Isabelle/ML.
+</p>
+
+<p>
+  <b>Isabelle/jEdit</b> is an example application within the PIDE
+  framework &mdash; it illustrates many of the ideas in a realistic
+  manner, ready to be used right now in Isabelle applications.
+</p>
 
-The Isabelle/Scala layer that is already part of Isabelle/Pure
-provides some general infrastructure for advanced prover interaction
-and integration.  The Isabelle/jEdit application serves as an example
-for asynchronous proof checking with support for parallel processing.
+<p>
+  <em>Research and implementation of concepts around PIDE has been
+  kindly supported in the past 3 years by BMBF (http://www.bmbf.de),
+  Université Paris-Sud (http://www.u-psud.fr), and Digiteo
+  (http://www.digiteo.fr).</em>
+</p>
+
+
+
+<h2>The Isabelle/jEdit Prover IDE</h2>
+
+<p>
+Isabelle/jEdit consists of some plugins for the well-known jEdit text
+editor framework (http://www.jedit.org), according to the following
+principles.
+</p>
 
 <ul>
 
@@ -35,18 +61,21 @@
 
 <li>Using the mouse together with the modifier key <tt>C</tt>
 (<tt>CONTROL</tt> on Linux or Windows,
-  <tt>COMMAND</tt> on Mac OS) exposes additional information.</li>
+  <tt>COMMAND</tt> on Mac OS X) exposes additional information.</li>
 
 <li>Dockable panels (e.g. <em>Output</em>) are managed as independent
   windows by jEdit, which also allows multiple instances.</li>
 
+<li>Prover process and source files are managed by the Scala layer on
+the editor side.  The prover experiences a mostly timeless and
+stateless environment of formal document content.</li>
+
 </ul>
 
 
 <h2>Isabelle symbols and fonts</h2>
 
 <ul>
-
   <li>Isabelle supports infinitely many symbols:<br/>
     α, β, γ, …<br/>
     ∀, ∃, ∨, ∧, ⟶, ⟷, …<br/>
@@ -118,10 +147,16 @@
     as the Unicode sequences coincide with the symbol mapping.
   </li>
 
+  <li><b>NOTE:</b> Raw unicode characters within prover source files
+  should be restricted to informal parts, e.g. to write text in
+  non-latin alphabets.  Mathematical symbols should be defined via the
+  official rendering tables.
+  </li>
+
 </ul>
 
 
-<h2>Limitations and workrounds (September 2011)</h2>
+<h2>Limitations and workrounds (October 2011)</h2>
 
 <ul>
   <li>No way to start/stop prover or switch to a different logic.<br/>
@@ -158,7 +193,7 @@
 </ul>
 
 
-<h2>Known problems with Mac OS</h2>
+<h2>Known problems with Mac OS X</h2>
 
 <ul>
 
@@ -166,22 +201,21 @@
   e.g. between the editor and the Console plugin, which is a standard
   swing text box.  Similar for search boxes etc.</li>
 
-<li>ToggleButton selected state is not rendered if window focus is
-  lost, which is probably a genuine feature of the Apple
-  look-and-feel.</li>
-
-<li>Font.createFont mangles the font family of non-regular fonts,
-  e.g. bold.  IsabelleText font files need to be installed/updated
-  manually.</li>
+<li><tt>Font.createFont</tt> mangles the font family of non-regular
+  fonts, e.g. bold.  IsabelleText font files need to be
+  installed/updated manually if bold versions are desired.  Note that
+  this has to be repeated whenever fonts shipped with Isabelle are
+  updated!</li>
 
 <li>Missing glyphs are collected from other fonts (like Emacs,
-  Firefox).  This is actually an advantage over the Oracle/Sun JVM on
-  Windows or Linux, but probably also the deeper reason for the other
-  oddities of Apple font management.</li>
+  Firefox).  This is actually an advantage over the Oracle JVM on
+  Windows or Linux, but also the deeper reason for other oddities of
+  Apple font management.</li>
 
-<li>The native font renderer of -Dapple.awt.graphics.UseQuartz=true
-  (not enabled by default) fails to handle the infinitesimal font size
-  of "hidden" text (e.g.  used in Isabelle sub/superscripts).</li>
+<li>The native font renderer
+  of <tt>-Dapple.awt.graphics.UseQuartz=true</tt> (<em>not</em>
+  enabled by default) fails to handle the infinitesimal font size of
+  "hidden" text (e.g. used in Isabelle sub/superscripts).</li>
 
 </ul>
 
@@ -191,23 +225,10 @@
 <ul>
 
 <li>The 2D rendering engine of OpenJDK 1.6.x distorts the appearance
-  of the jEdit text area.  Always use official JRE 1.6.x from
-  Sun/Oracle/Apple.</li>
-
-<li>jEdit on OpenJDK is generally not supported.</li>
-
-</ul>
-
+  of the jEdit text area.  Always use official JRE 1.6.x from Oracle
+  or Apple.</li>
 
-<h2>Known problems with Windows/Cygwin</h2>
-
-<ul>
-
-<li>Occasional session startup problems when loading a logic image
-takes too long (cf. output in "Prover Session / Syslog" panel).</li>
-
-<li>Auxiliary files of a theory (<tt>uses</tt>) cannot be loaded due
-to incompatible path notation inherited from MS-DOS.</li>
+<li>jEdit 4.4.x on OpenJDK is generally not supported.</li>
 
 </ul>
 
@@ -216,6 +237,8 @@
 
 <ul>
 
+<li>Isabelle: BSD-style</li>
+
 <li>Scala: BSD-style <br/> http://www.scala-lang.org</li>
 
 <li>jEdit: GPL (with special cases) <br/> http://www.jedit.org/</li>
diff -r 49e305100097 -r d78ec6c10fa1 src/Tools/jEdit/src/html_panel.scala
--- a/src/Tools/jEdit/src/html_panel.scala	Sun Oct 09 11:13:53 2011 +0200
+++ b/src/Tools/jEdit/src/html_panel.scala	Mon Oct 10 11:12:09 2011 +0200
@@ -113,7 +113,7 @@
   /* internal messages */
 
   private case class Resize(font_family: String, font_size: Int)
-  private case class Render_Document(text: String)
+  private case class Render_Document(url: String, text: String)
   private case class Render(body: XML.Body)
   private case class Render_Sync(body: XML.Body)
   private case object Refresh
@@ -151,9 +151,9 @@
 
     def refresh() { render(current_body) }
 
-    def render_document(text: String)
+    def render_document(url: String, text: String)
     {
-      val doc = builder.parse(new InputSourceImpl(new StringReader(text), "http://localhost"))
+      val doc = builder.parse(new InputSourceImpl(new StringReader(text), url))
       Swing_Thread.later { setDocument(doc, rcontext) }
     }
 
@@ -183,7 +183,7 @@
       react {
         case Resize(font_family, font_size) => resize(font_family, font_size)
         case Refresh => refresh()
-        case Render_Document(text) => render_document(text)
+        case Render_Document(url, text) => render_document(url, text)
         case Render(body) => render(body)
         case Render_Sync(body) => render(body); reply(())
         case bad => System.err.println("main_actor: ignoring bad message " + bad)
@@ -196,7 +196,7 @@
 
   def resize(font_family: String, font_size: Int) { main_actor ! Resize(font_family, font_size) }
   def refresh() { main_actor ! Refresh }
-  def render_document(text: String) { main_actor ! Render_Document(text) }
+  def render_document(url: String, text: String) { main_actor ! Render_Document(url, text) }
   def render(body: XML.Body) { main_actor ! Render(body) }
   def render_sync(body: XML.Body) { main_actor !? Render_Sync(body) }
 }
diff -r 49e305100097 -r d78ec6c10fa1 src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Sun Oct 09 11:13:53 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Mon Oct 10 11:12:09 2011 +0200
@@ -27,7 +27,10 @@
   /* main tabs */
 
   private val readme = new HTML_Panel("SansSerif", 14)
-  readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
+  private val readme_path = Path.explode("$JEDIT_HOME/README.html")
+  readme.render_document(
+    Isabelle_System.platform_file_url(readme_path),
+    Isabelle_System.try_read(List(readme_path)))
 
   val status = new ListView(Nil: List[Document.Node.Name]) {
     listenTo(mouse.clicks)
diff -r 49e305100097 -r d78ec6c10fa1 src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Sun Oct 09 11:13:53 2011 +0200
+++ b/src/Tools/subtyping.ML	Mon Oct 10 11:12:09 2011 +0200
@@ -628,7 +628,7 @@
                 NONE => raise COERCION_GEN_ERROR (err ++> quote (Syntax.string_of_typ ctxt T1) ^
                   " is not a subtype of " ^ quote (Syntax.string_of_typ ctxt T2))
               | SOME (co, _) => co)
-      | ((Type (a, Ts)), (Type (b, Us))) =>
+      | (T1 as Type (a, Ts), T2 as Type (b, Us)) =>
             if a <> b
             then
               (case Symreltab.lookup (coes_of ctxt) (a, b) of
@@ -656,8 +656,11 @@
                   | ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs);
               in
                 (case Symtab.lookup (tmaps_of ctxt) a of
-                  NONE => raise COERCION_GEN_ERROR
-                    (err ++> "No map function for " ^ quote a ^ " known")
+                  NONE =>
+                    if Type.could_unify (T1, T2)
+                    then Abs (Name.uu, T1, Bound 0)
+                    else raise COERCION_GEN_ERROR
+                      (err ++> "No map function for " ^ quote a ^ " known")
                 | SOME tmap =>
                     let
                       val used_coes = map_filter sub_co ((snd tmap) ~~ (Ts ~~ Us));