# HG changeset patch
# User blanchet
# Date 1283377625 -7200
# Node ID 83ca64a880eaac81d075b365f81c90671bdefeaa
# Parent  aae6a0d33c665f96a34f4e0758ae678b06f66611
handle all whitespace, not just ASCII 32

diff -r aae6a0d33c66 -r 83ca64a880ea src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Sep 01 23:41:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Sep 01 23:47:05 2010 +0200
@@ -177,7 +177,7 @@
 val extract_clause_formula_relation =
   Substring.full #> Substring.position set_ClauseFormulaRelationN
   #> snd #> Substring.position "." #> fst #> Substring.string
-  #> explode #> filter_out (curry (op =) " ") #> parse_clause_formula_relation
+  #> explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
   #> fst
 
 (* TODO: move to "Sledgehammer_Reconstruct" *)