# HG changeset patch
# User wenzelm
# Date 1129327760 -7200
# Node ID 5a12b1b5990f0e60fab39675d1b473a444ce9ec3
# Parent  3368e5c7290484b824ffae9302f8d9b9df34cf7d
tuned comment;

diff -r 3368e5c72904 -r 5a12b1b5990f src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Oct 15 00:09:07 2005 +0200
+++ b/src/Pure/thm.ML	Sat Oct 15 00:09:20 2005 +0200
@@ -1251,7 +1251,7 @@
 (*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;