1.1 --- a/.hgtags Sun Oct 09 11:13:53 2011 +0200
1.2 +++ b/.hgtags Mon Oct 10 11:12:09 2011 +0200
1.3 @@ -27,3 +27,5 @@
1.4 6a973bd4394996c31f638e5c59ea6bb953335c9a Isabelle2009-1
1.5 35815ce9218a8822a50f5d80b96aa8d1970ec35d Isabelle2009-2
1.6 6d736d983d5cfec4a6c6fba174db2cd93493a96b Isabelle2011
1.7 +76fef3e570043b84a32716b5633085d2fb215525 Isabelle2011-1
1.8 +
2.1 --- a/Admin/CHECKLIST Sun Oct 09 11:13:53 2011 +0200
2.2 +++ b/Admin/CHECKLIST Mon Oct 10 11:12:09 2011 +0200
2.3 @@ -42,12 +42,12 @@
2.4
2.5 - makebin (multiplatform);
2.6
2.7 -- makebin -l on fast machine;
2.8 -
2.9 - makebundle (multiplatform);
2.10
2.11 - hdiutil create -srcfolder DIR DMG (Mac OS);
2.12
2.13 +- makebin -l on fast machine, based on renamed bundle with deleted heaps;
2.14 +
2.15
2.16 Final release stage
2.17 ===================
3.1 --- a/Admin/MacOS/App1/script Sun Oct 09 11:13:53 2011 +0200
3.2 +++ b/Admin/MacOS/App1/script Mon Oct 10 11:12:09 2011 +0200
3.3 @@ -106,8 +106,7 @@
3.4 ( "$ISABELLE_TOOL" emacs "${EMACS_OPTIONS[@]}" "$@" ) > "$OUTPUT" 2>&1
3.5 RC=$?
3.6 else
3.7 - rm -f "$OUTPUT" && touch "$OUTPUT"
3.8 - "$ISABELLE_TOOL" jedit "$@"
3.9 + ( "$ISABELLE_TOOL" jedit "$@" ) > "$OUTPUT" 2>&1
3.10 RC=$?
3.11 fi
3.12
4.1 --- a/Admin/build Sun Oct 09 11:13:53 2011 +0200
4.2 +++ b/Admin/build Mon Oct 10 11:12:09 2011 +0200
4.3 @@ -84,7 +84,7 @@
4.4
4.5 function build_jars ()
4.6 {
4.7 - "$ISABELLE_HOME/lib/scripts/java_ext_dirs" >/dev/null
4.8 + "$ISABELLE_TOOL" env "$ISABELLE_HOME/lib/scripts/java_ext_dirs" >/dev/null
4.9 pushd "$ISABELLE_HOME/src/Pure" >/dev/null
4.10 "$ISABELLE_TOOL" env ./build-jars "$@" || exit $?
4.11 popd >/dev/null
5.1 --- a/Admin/makedist Sun Oct 09 11:13:53 2011 +0200
5.2 +++ b/Admin/makedist Mon Oct 10 11:12:09 2011 +0200
5.3 @@ -178,7 +178,6 @@
5.4 echo
5.5 } >ANNOUNCE
5.6 else
5.7 - rm Isabelle Isabelle.exe
5.8 perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML
5.9 fi
5.10
6.1 --- a/doc-src/IsarRef/Thy/First_Order_Logic.thy Sun Oct 09 11:13:53 2011 +0200
6.2 +++ b/doc-src/IsarRef/Thy/First_Order_Logic.thy Mon Oct 10 11:12:09 2011 +0200
6.3 @@ -47,7 +47,7 @@
6.4 text {*
6.5 \noindent Substitution is very powerful, but also hard to control in
6.6 full generality. We derive some common symmetry~/ transitivity
6.7 - schemes of as particular consequences.
6.8 + schemes of @{term equal} as particular consequences.
6.9 *}
6.10
6.11 theorem sym [sym]:
7.1 --- a/doc-src/IsarRef/Thy/Proof.thy Sun Oct 09 11:13:53 2011 +0200
7.2 +++ b/doc-src/IsarRef/Thy/Proof.thy Mon Oct 10 11:12:09 2011 +0200
7.3 @@ -129,7 +129,7 @@
7.4 proof structure at all, but goes back right to the theory level.
7.5 Furthermore, @{command "oops"} does not produce any result theorem
7.6 --- there is no intended claim to be able to complete the proof
7.7 - anyhow.
7.8 + in any way.
7.9
7.10 A typical application of @{command "oops"} is to explain Isar proofs
7.11 \emph{within} the system itself, in conjunction with the document
8.1 --- a/doc-src/IsarRef/Thy/Synopsis.thy Sun Oct 09 11:13:53 2011 +0200
8.2 +++ b/doc-src/IsarRef/Thy/Synopsis.thy Mon Oct 10 11:12:09 2011 +0200
8.3 @@ -907,7 +907,7 @@
8.4
8.5 text {* There is nothing special about logical connectives (@{text
8.6 "\<and>"}, @{text "\<or>"}, @{text "\<forall>"}, @{text "\<exists>"} etc.). Operators from
8.7 - set-theory or lattice-theory for analogously. It is only a matter
8.8 + set-theory or lattice-theory work analogously. It is only a matter
8.9 of rule declarations in the library; rules can be also specified
8.10 explicitly.
8.11 *}
8.12 @@ -1105,4 +1105,4 @@
8.13 note `C`
8.14 end
8.15
8.16 -end
8.17 \ No newline at end of file
8.18 +end
9.1 --- a/doc-src/IsarRef/Thy/document/First_Order_Logic.tex Sun Oct 09 11:13:53 2011 +0200
9.2 +++ b/doc-src/IsarRef/Thy/document/First_Order_Logic.tex Mon Oct 10 11:12:09 2011 +0200
9.3 @@ -68,7 +68,7 @@
9.4 \begin{isamarkuptext}%
9.5 \noindent Substitution is very powerful, but also hard to control in
9.6 full generality. We derive some common symmetry~/ transitivity
9.7 - schemes of as particular consequences.%
9.8 + schemes of \isa{equal} as particular consequences.%
9.9 \end{isamarkuptext}%
9.10 \isamarkuptrue%
9.11 \isacommand{theorem}\isamarkupfalse%
10.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex Sun Oct 09 11:13:53 2011 +0200
10.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex Mon Oct 10 11:12:09 2011 +0200
10.3 @@ -159,7 +159,7 @@
10.4 proof structure at all, but goes back right to the theory level.
10.5 Furthermore, \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} does not produce any result theorem
10.6 --- there is no intended claim to be able to complete the proof
10.7 - anyhow.
10.8 + in any way.
10.9
10.10 A typical application of \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} is to explain Isar proofs
10.11 \emph{within} the system itself, in conjunction with the document
11.1 --- a/doc-src/IsarRef/Thy/document/Synopsis.tex Sun Oct 09 11:13:53 2011 +0200
11.2 +++ b/doc-src/IsarRef/Thy/document/Synopsis.tex Mon Oct 10 11:12:09 2011 +0200
11.3 @@ -2258,7 +2258,7 @@
11.4 %
11.5 \begin{isamarkuptext}%
11.6 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
11.7 - set-theory or lattice-theory for analogously. It is only a matter
11.8 + set-theory or lattice-theory work analogously. It is only a matter
11.9 of rule declarations in the library; rules can be also specified
11.10 explicitly.%
11.11 \end{isamarkuptext}%
11.12 @@ -2708,6 +2708,7 @@
11.13 {\isafoldtheory}%
11.14 %
11.15 \isadelimtheory
11.16 +\isanewline
11.17 %
11.18 \endisadelimtheory
11.19 \end{isabellebody}%
12.1 --- a/doc-src/TutorialI/Documents/Documents.thy Sun Oct 09 11:13:53 2011 +0200
12.2 +++ b/doc-src/TutorialI/Documents/Documents.thy Mon Oct 10 11:12:09 2011 +0200
12.3 @@ -344,7 +344,7 @@
12.4 session is derived from a single parent, usually an object-logic
12.5 image like \texttt{HOL}. This results in an overall tree structure,
12.6 which is reflected by the output location in the file system
12.7 - (usually rooted at \verb,~/.isabelle/browser_info,).
12.8 + (usually rooted at \verb,~/.isabelle/IsabelleXXXX/browser_info,).
12.9
12.10 \medskip The easiest way to manage Isabelle sessions is via
12.11 \texttt{isabelle mkdir} (generates an initial session source setup)
13.1 --- a/doc-src/TutorialI/Documents/document/Documents.tex Sun Oct 09 11:13:53 2011 +0200
13.2 +++ b/doc-src/TutorialI/Documents/document/Documents.tex Mon Oct 10 11:12:09 2011 +0200
13.3 @@ -417,7 +417,7 @@
13.4 session is derived from a single parent, usually an object-logic
13.5 image like \texttt{HOL}. This results in an overall tree structure,
13.6 which is reflected by the output location in the file system
13.7 - (usually rooted at \verb,~/.isabelle/browser_info,).
13.8 + (usually rooted at \verb,~/.isabelle/IsabelleXXXX/browser_info,).
13.9
13.10 \medskip The easiest way to manage Isabelle sessions is via
13.11 \texttt{isabelle mkdir} (generates an initial session source setup)
14.1 --- a/etc/user-settings.sample Sun Oct 09 11:13:53 2011 +0200
14.2 +++ b/etc/user-settings.sample Mon Oct 10 11:12:09 2011 +0200
14.3 @@ -1,6 +1,6 @@
14.4 # -*- shell-script -*- :mode=shellscript:
14.5 #
14.6 -# Isabelle user settings sample -- for use in ~/.isabelle/etc/settings
14.7 +# Isabelle user settings sample -- for use in $ISABELLE_HOME_USER/etc/settings
14.8
14.9 ISABELLE_USEDIR_OPTIONS="-i true -d pdf"
14.10 ISABELLE_LOGIC=HOL
15.1 --- a/lib/Tools/java Sun Oct 09 11:13:53 2011 +0200
15.2 +++ b/lib/Tools/java Mon Oct 10 11:12:09 2011 +0200
15.3 @@ -8,6 +8,13 @@
15.4
15.5 JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
15.6
15.7 +if "$JAVA_EXE" -version >/dev/null 2>/dev/null; then
15.8 + :
15.9 +else
15.10 + echo "Bad Java executable: \"$JAVA_EXE\"" >&2
15.11 + exit 2
15.12 +fi
15.13 +
15.14 if "$JAVA_EXE" -server >/dev/null 2>/dev/null; then
15.15 SERVER="-server"
15.16 else
16.1 --- a/lib/scripts/getsettings Sun Oct 09 11:13:53 2011 +0200
16.2 +++ b/lib/scripts/getsettings Mon Oct 10 11:12:09 2011 +0200
16.3 @@ -14,7 +14,7 @@
16.4 export ISABELLE_HOME
16.5 if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; }
16.6 then
16.7 - echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems later on!"
16.8 + echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems!"
16.9 echo 1>&2 "### ISABELLE_HOME=\"$ISABELLE_HOME\""
16.10 fi
16.11
17.1 --- a/src/Pure/System/isabelle_system.scala Sun Oct 09 11:13:53 2011 +0200
17.2 +++ b/src/Pure/System/isabelle_system.scala Mon Oct 10 11:12:09 2011 +0200
17.3 @@ -110,6 +110,16 @@
17.4 def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path))
17.5 def platform_file(path: Path): File = new File(platform_path(path))
17.6
17.7 + def platform_file_url(raw_path: Path): String =
17.8 + {
17.9 + val path = raw_path.expand
17.10 + require(path.is_absolute)
17.11 + val s = platform_path(path).replaceAll(" ", "%20")
17.12 + if (!Platform.is_windows) "file://" + s
17.13 + else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
17.14 + else "file:///" + s.replace('\\', '/')
17.15 + }
17.16 +
17.17 def posix_path(jvm_path: String): String = standard_system.posix_path(jvm_path)
17.18
17.19
18.1 Binary file src/Tools/jEdit/PIDE.png has changed
19.1 --- a/src/Tools/jEdit/README.html Sun Oct 09 11:13:53 2011 +0200
19.2 +++ b/src/Tools/jEdit/README.html Mon Oct 10 11:12:09 2011 +0200
19.3 @@ -7,17 +7,43 @@
19.4 <style type="text/css" media="screen">
19.5 body { font-family: STIXGeneral, IsabelleText; font-size: 14pt; }
19.6 </style>
19.7 -<title>Notes on the Isabelle/jEdit Prover IDE</title>
19.8 +<title>Welcome to the Isabelle/jEdit Prover IDE</title>
19.9 </head>
19.10
19.11 <body>
19.12
19.13 -<h2>The Isabelle/jEdit Prover IDE (based on Isabelle/Scala)</h2>
19.14 +<center><h2><img alt="PIDE" src="PIDE.png" width="230" align="middle"/></h2></center>
19.15
19.16 -The Isabelle/Scala layer that is already part of Isabelle/Pure
19.17 -provides some general infrastructure for advanced prover interaction
19.18 -and integration. The Isabelle/jEdit application serves as an example
19.19 -for asynchronous proof checking with support for parallel processing.
19.20 +<p>
19.21 + <b>PIDE</b> is a novel framework for sophisticated Prover IDEs,
19.22 + based on Isabelle/Scala technology that is integrated with Isabelle.
19.23 + It is build around a concept of
19.24 + <em>asynchronous document processing</em>, which is supported
19.25 + natively by the <em>parallel proof engine</em> implemented in Isabelle/ML.
19.26 +</p>
19.27 +
19.28 +<p>
19.29 + <b>Isabelle/jEdit</b> is an example application within the PIDE
19.30 + framework — it illustrates many of the ideas in a realistic
19.31 + manner, ready to be used right now in Isabelle applications.
19.32 +</p>
19.33 +
19.34 +<p>
19.35 + <em>Research and implementation of concepts around PIDE has been
19.36 + kindly supported in the past 3 years by BMBF (http://www.bmbf.de),
19.37 + Université Paris-Sud (http://www.u-psud.fr), and Digiteo
19.38 + (http://www.digiteo.fr).</em>
19.39 +</p>
19.40 +
19.41 +
19.42 +
19.43 +<h2>The Isabelle/jEdit Prover IDE</h2>
19.44 +
19.45 +<p>
19.46 +Isabelle/jEdit consists of some plugins for the well-known jEdit text
19.47 +editor framework (http://www.jedit.org), according to the following
19.48 +principles.
19.49 +</p>
19.50
19.51 <ul>
19.52
19.53 @@ -35,18 +61,21 @@
19.54
19.55 <li>Using the mouse together with the modifier key <tt>C</tt>
19.56 (<tt>CONTROL</tt> on Linux or Windows,
19.57 - <tt>COMMAND</tt> on Mac OS) exposes additional information.</li>
19.58 + <tt>COMMAND</tt> on Mac OS X) exposes additional information.</li>
19.59
19.60 <li>Dockable panels (e.g. <em>Output</em>) are managed as independent
19.61 windows by jEdit, which also allows multiple instances.</li>
19.62
19.63 +<li>Prover process and source files are managed by the Scala layer on
19.64 +the editor side. The prover experiences a mostly timeless and
19.65 +stateless environment of formal document content.</li>
19.66 +
19.67 </ul>
19.68
19.69
19.70 <h2>Isabelle symbols and fonts</h2>
19.71
19.72 <ul>
19.73 -
19.74 <li>Isabelle supports infinitely many symbols:<br/>
19.75 α, β, γ, …<br/>
19.76 ∀, ∃, ∨, ∧, ⟶, ⟷, …<br/>
19.77 @@ -118,10 +147,16 @@
19.78 as the Unicode sequences coincide with the symbol mapping.
19.79 </li>
19.80
19.81 + <li><b>NOTE:</b> Raw unicode characters within prover source files
19.82 + should be restricted to informal parts, e.g. to write text in
19.83 + non-latin alphabets. Mathematical symbols should be defined via the
19.84 + official rendering tables.
19.85 + </li>
19.86 +
19.87 </ul>
19.88
19.89
19.90 -<h2>Limitations and workrounds (September 2011)</h2>
19.91 +<h2>Limitations and workrounds (October 2011)</h2>
19.92
19.93 <ul>
19.94 <li>No way to start/stop prover or switch to a different logic.<br/>
19.95 @@ -158,7 +193,7 @@
19.96 </ul>
19.97
19.98
19.99 -<h2>Known problems with Mac OS</h2>
19.100 +<h2>Known problems with Mac OS X</h2>
19.101
19.102 <ul>
19.103
19.104 @@ -166,22 +201,21 @@
19.105 e.g. between the editor and the Console plugin, which is a standard
19.106 swing text box. Similar for search boxes etc.</li>
19.107
19.108 -<li>ToggleButton selected state is not rendered if window focus is
19.109 - lost, which is probably a genuine feature of the Apple
19.110 - look-and-feel.</li>
19.111 -
19.112 -<li>Font.createFont mangles the font family of non-regular fonts,
19.113 - e.g. bold. IsabelleText font files need to be installed/updated
19.114 - manually.</li>
19.115 +<li><tt>Font.createFont</tt> mangles the font family of non-regular
19.116 + fonts, e.g. bold. IsabelleText font files need to be
19.117 + installed/updated manually if bold versions are desired. Note that
19.118 + this has to be repeated whenever fonts shipped with Isabelle are
19.119 + updated!</li>
19.120
19.121 <li>Missing glyphs are collected from other fonts (like Emacs,
19.122 - Firefox). This is actually an advantage over the Oracle/Sun JVM on
19.123 - Windows or Linux, but probably also the deeper reason for the other
19.124 - oddities of Apple font management.</li>
19.125 + Firefox). This is actually an advantage over the Oracle JVM on
19.126 + Windows or Linux, but also the deeper reason for other oddities of
19.127 + Apple font management.</li>
19.128
19.129 -<li>The native font renderer of -Dapple.awt.graphics.UseQuartz=true
19.130 - (not enabled by default) fails to handle the infinitesimal font size
19.131 - of "hidden" text (e.g. used in Isabelle sub/superscripts).</li>
19.132 +<li>The native font renderer
19.133 + of <tt>-Dapple.awt.graphics.UseQuartz=true</tt> (<em>not</em>
19.134 + enabled by default) fails to handle the infinitesimal font size of
19.135 + "hidden" text (e.g. used in Isabelle sub/superscripts).</li>
19.136
19.137 </ul>
19.138
19.139 @@ -191,23 +225,10 @@
19.140 <ul>
19.141
19.142 <li>The 2D rendering engine of OpenJDK 1.6.x distorts the appearance
19.143 - of the jEdit text area. Always use official JRE 1.6.x from
19.144 - Sun/Oracle/Apple.</li>
19.145 + of the jEdit text area. Always use official JRE 1.6.x from Oracle
19.146 + or Apple.</li>
19.147
19.148 -<li>jEdit on OpenJDK is generally not supported.</li>
19.149 -
19.150 -</ul>
19.151 -
19.152 -
19.153 -<h2>Known problems with Windows/Cygwin</h2>
19.154 -
19.155 -<ul>
19.156 -
19.157 -<li>Occasional session startup problems when loading a logic image
19.158 -takes too long (cf. output in "Prover Session / Syslog" panel).</li>
19.159 -
19.160 -<li>Auxiliary files of a theory (<tt>uses</tt>) cannot be loaded due
19.161 -to incompatible path notation inherited from MS-DOS.</li>
19.162 +<li>jEdit 4.4.x on OpenJDK is generally not supported.</li>
19.163
19.164 </ul>
19.165
19.166 @@ -216,6 +237,8 @@
19.167
19.168 <ul>
19.169
19.170 +<li>Isabelle: BSD-style</li>
19.171 +
19.172 <li>Scala: BSD-style <br/> http://www.scala-lang.org</li>
19.173
19.174 <li>jEdit: GPL (with special cases) <br/> http://www.jedit.org/</li>
20.1 --- a/src/Tools/jEdit/src/html_panel.scala Sun Oct 09 11:13:53 2011 +0200
20.2 +++ b/src/Tools/jEdit/src/html_panel.scala Mon Oct 10 11:12:09 2011 +0200
20.3 @@ -113,7 +113,7 @@
20.4 /* internal messages */
20.5
20.6 private case class Resize(font_family: String, font_size: Int)
20.7 - private case class Render_Document(text: String)
20.8 + private case class Render_Document(url: String, text: String)
20.9 private case class Render(body: XML.Body)
20.10 private case class Render_Sync(body: XML.Body)
20.11 private case object Refresh
20.12 @@ -151,9 +151,9 @@
20.13
20.14 def refresh() { render(current_body) }
20.15
20.16 - def render_document(text: String)
20.17 + def render_document(url: String, text: String)
20.18 {
20.19 - val doc = builder.parse(new InputSourceImpl(new StringReader(text), "http://localhost"))
20.20 + val doc = builder.parse(new InputSourceImpl(new StringReader(text), url))
20.21 Swing_Thread.later { setDocument(doc, rcontext) }
20.22 }
20.23
20.24 @@ -183,7 +183,7 @@
20.25 react {
20.26 case Resize(font_family, font_size) => resize(font_family, font_size)
20.27 case Refresh => refresh()
20.28 - case Render_Document(text) => render_document(text)
20.29 + case Render_Document(url, text) => render_document(url, text)
20.30 case Render(body) => render(body)
20.31 case Render_Sync(body) => render(body); reply(())
20.32 case bad => System.err.println("main_actor: ignoring bad message " + bad)
20.33 @@ -196,7 +196,7 @@
20.34
20.35 def resize(font_family: String, font_size: Int) { main_actor ! Resize(font_family, font_size) }
20.36 def refresh() { main_actor ! Refresh }
20.37 - def render_document(text: String) { main_actor ! Render_Document(text) }
20.38 + def render_document(url: String, text: String) { main_actor ! Render_Document(url, text) }
20.39 def render(body: XML.Body) { main_actor ! Render(body) }
20.40 def render_sync(body: XML.Body) { main_actor !? Render_Sync(body) }
20.41 }
21.1 --- a/src/Tools/jEdit/src/session_dockable.scala Sun Oct 09 11:13:53 2011 +0200
21.2 +++ b/src/Tools/jEdit/src/session_dockable.scala Mon Oct 10 11:12:09 2011 +0200
21.3 @@ -27,7 +27,10 @@
21.4 /* main tabs */
21.5
21.6 private val readme = new HTML_Panel("SansSerif", 14)
21.7 - readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
21.8 + private val readme_path = Path.explode("$JEDIT_HOME/README.html")
21.9 + readme.render_document(
21.10 + Isabelle_System.platform_file_url(readme_path),
21.11 + Isabelle_System.try_read(List(readme_path)))
21.12
21.13 val status = new ListView(Nil: List[Document.Node.Name]) {
21.14 listenTo(mouse.clicks)
22.1 --- a/src/Tools/subtyping.ML Sun Oct 09 11:13:53 2011 +0200
22.2 +++ b/src/Tools/subtyping.ML Mon Oct 10 11:12:09 2011 +0200
22.3 @@ -628,7 +628,7 @@
22.4 NONE => raise COERCION_GEN_ERROR (err ++> quote (Syntax.string_of_typ ctxt T1) ^
22.5 " is not a subtype of " ^ quote (Syntax.string_of_typ ctxt T2))
22.6 | SOME (co, _) => co)
22.7 - | ((Type (a, Ts)), (Type (b, Us))) =>
22.8 + | (T1 as Type (a, Ts), T2 as Type (b, Us)) =>
22.9 if a <> b
22.10 then
22.11 (case Symreltab.lookup (coes_of ctxt) (a, b) of
22.12 @@ -656,8 +656,11 @@
22.13 | ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs);
22.14 in
22.15 (case Symtab.lookup (tmaps_of ctxt) a of
22.16 - NONE => raise COERCION_GEN_ERROR
22.17 - (err ++> "No map function for " ^ quote a ^ " known")
22.18 + NONE =>
22.19 + if Type.could_unify (T1, T2)
22.20 + then Abs (Name.uu, T1, Bound 0)
22.21 + else raise COERCION_GEN_ERROR
22.22 + (err ++> "No map function for " ^ quote a ^ " known")
22.23 | SOME tmap =>
22.24 let
22.25 val used_coes = map_filter sub_co ((snd tmap) ~~ (Ts ~~ Us));