src/Pure/thm.ML

   (case  Logic.strip_prems(i, [], prop) of
       (B::rBs, C) => (tpairs, rev rBs, B, C)
     | _ => 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;
     val inc = gmax + 1;
     val lift_abs = Logic.lift_abs inc gprop;