src/Pure/tactic.ML
changeset 952 9e10962866b0
parent 949 83c588d6fee9
child 1077 c2df11ae8b55
     1.1 --- a/src/Pure/tactic.ML	Tue Mar 14 09:47:28 1995 +0100
     1.2 +++ b/src/Pure/tactic.ML	Tue Mar 14 10:40:04 1995 +0100
     1.3 @@ -220,15 +220,10 @@
     1.4    terms that are substituted contain (term or type) unknowns from the
     1.5    goal, because it is unable to instantiate goal unknowns at the same time.
     1.6  
     1.7 -  The type checker freezes all flexible type vars that were introduced during
     1.8 -  type inference and still remain in the term at the end.  This avoids the
     1.9 -  introduction of flexible type vars in goals and other places where they
    1.10 -  could cause complications.  If you really want a flexible type var, you
    1.11 -  have to put it in yourself as a constraint.
    1.12 -
    1.13 -  This policy breaks down when a list of substitutions is type checked: later
    1.14 -  pairs may force type instantiations in earlier pairs, which is impossible,
    1.15 -  because the type vars in the earlier pairs are already frozen.
    1.16 +  The type checker is instructed not to freezes flexible type vars that
    1.17 +  were introduced during type inference and still remain in the term at the
    1.18 +  end.  This increases flexibility but can introduce schematic type vars in
    1.19 +  goals.
    1.20  *)
    1.21  fun res_inst_tac sinsts rule i =
    1.22      compose_inst_tac sinsts (false, rule, nprems_of rule) i;