--- a/src/Pure/thm.ML Wed Jan 25 13:31:56 2012 +0100
+++ b/src/Pure/thm.ML Wed Jan 25 14:13:59 2012 +0100
@@ -1306,8 +1306,8 @@
| _ => raise THM("dest_state", i, [state]))
handle TERM _ => raise THM("dest_state", i, [state]);
-(*Increment variables and parameters of orule as required for
- resolution with a goal.*)
+(*Prepare orule for resolution by lifting it over the parameters and
+assumptions of goal.*)
fun lift_rule goal orule =
let
val Cterm {t = gprop, T, maxidx = gmax, sorts, ...} = goal;