--- 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 =