# HG changeset patch
# User lcp
# Date 786882385 -3600
# Node ID 04320c2955006bf4ef4481a79ef1603b0a8ba94e
# Parent  f0200e91b272d73a581c0605dca0c6a71ba70b3c
res_inst_tac: added comments

diff -r f0200e91b272 -r 04320c295500 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Wed Dec 07 13:12:04 1994 +0100
+++ b/src/Pure/tactic.ML	Thu Dec 08 11:26:25 1994 +0100
@@ -213,7 +213,20 @@
 	   handle TERM (msg,_) => (writeln msg;  no_tac)
 		| THM  (msg,_,_) => (writeln msg;  no_tac) );
 
-(*Resolve version*)
+(*"Resolve" version.  Note: res_inst_tac cannot behave sensibly if the
+  terms that are substituted contain (term or type) unknowns from the
+  goal, because it is unable to instantiate goal unknowns at the same time.
+
+  The type checker freezes all flexible type vars that were introduced during
+  type inference and still remain in the term at the end.  This avoids the
+  introduction of flexible type vars in goals and other places where they
+  could cause complications.  If you really want a flexible type var, you
+  have to put it in yourself as a constraint.
+
+  This policy breaks down when a list of substitutions is type checked: later
+  pairs may force type instantiations in earlier pairs, which is impossible,
+  because the type vars in the earlier pairs are already frozen.
+*)
 fun res_inst_tac sinsts rule i =
     compose_inst_tac sinsts (false, rule, nprems_of rule) i;