src/Pure/thm.ML

 (** User renaming of parameters in a subgoal **)
 
 (*Calls error rather than raising an exception because it is intended
   for top-level use -- exception handling would not make sense here.
   The names in cs, if distinct, are used for the innermost parameters;
-   preceding parameters may be renamed to make all params distinct.*)
+  preceding parameters may be renamed to make all params distinct.*)
 fun rename_params_rule (cs, i) state =
   let
     val Thm {thy_ref, der, maxidx, shyps, hyps, ...} = state;
     val (tpairs, Bs, Bi, C) = dest_state (state, i);
     val iparams = map #1 (Logic.strip_params Bi);