# HG changeset patch
# User paulson
# Date 1077183435 -3600
# Node ID 51b24127eef2124119390a6bce5cd1789049f2a0
# Parent  71dff3bade664cdb3e5ec76bc10bac9466ae9f7e
comments!!

diff -r 71dff3bade66 -r 51b24127eef2 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Feb 18 16:01:37 2004 +0100
+++ b/src/Pure/drule.ML	Thu Feb 19 10:37:15 2004 +0100
@@ -368,9 +368,11 @@
     in Thm.instantiate (ctye, varpairs(vars,rev bs)) th end;
 
 
-(*Standard form of object-rule: no hypotheses, Frees, or outer quantifiers;
-    all generality expressed by Vars having index 0.*)
+(** Standard form of object-rule: no hypotheses, flexflex constraints,
+    Frees, or outer quantifiers; all generality expressed by Vars of index 0.**)
 
+(*Squash a theorem's flexflex constraints provided it can be done uniquely.
+  This step can lose information.*)
 fun flexflex_unique th =
     case Seq.chop (2, flexflex_rule th) of
       ([th],_) => th