src/Pure/drule.ML
changeset 14394 51b24127eef2
parent 14391 bb726050650d
child 14643 130076a81b84
     1.1 --- a/src/Pure/drule.ML	Wed Feb 18 16:01:37 2004 +0100
     1.2 +++ b/src/Pure/drule.ML	Thu Feb 19 10:37:15 2004 +0100
     1.3 @@ -368,9 +368,11 @@
     1.4      in Thm.instantiate (ctye, varpairs(vars,rev bs)) th end;
     1.5  
     1.6  
     1.7 -(*Standard form of object-rule: no hypotheses, Frees, or outer quantifiers;
     1.8 -    all generality expressed by Vars having index 0.*)
     1.9 +(** Standard form of object-rule: no hypotheses, flexflex constraints,
    1.10 +    Frees, or outer quantifiers; all generality expressed by Vars of index 0.**)
    1.11  
    1.12 +(*Squash a theorem's flexflex constraints provided it can be done uniquely.
    1.13 +  This step can lose information.*)
    1.14  fun flexflex_unique th =
    1.15      case Seq.chop (2, flexflex_rule th) of
    1.16        ([th],_) => th