# HG changeset patch
# User blanchet
# Date 1316613315 -7200
# Node ID b0f61dec677ad1f0c37b5d04381fd184d6582e60
# Parent  34e5fc15ea0231bc08e8ee0dd83f67f4b7061543
tuned comment

diff -r 34e5fc15ea02 -r b0f61dec677a src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Sep 21 06:41:34 2011 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Sep 21 15:55:15 2011 +0200
@@ -149,13 +149,13 @@
     |> snd
   end
 
-(* This is a terrible hack. Free variables are sometimes code as "M__" when they
-   are displayed as "M" and we want to avoid clashes with these. But sometimes
-   it's even worse: "Ma__" encodes "M". So we simply reserve all prefixes of all
-   free variables. In the worse case scenario, where the fact won't be resolved
-   correctly, the user can fix it manually, e.g., by naming the fact in
-   question. Ideally we would need nothing of it, but backticks just don't work
-   with schematic variables. *)
+(* This is a terrible hack. Free variables are sometimes coded as "M__" when
+   they are displayed as "M" and we want to avoid clashes with these. But
+   sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all
+   prefixes of all free variables. In the worse case scenario, where the fact
+   won't be resolved correctly, the user can fix it manually, e.g., by naming
+   the fact in question. Ideally we would need nothing of it, but backticks
+   simply don't work with schematic variables. *)
 fun all_prefixes_of s =
   map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
 fun close_form t =