changeset 36183 | f723348b2231 |
parent 36170 | 0cdb76723c88 |
child 36378 | f32c567dbcaa |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Apr 16 16:08:43 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Apr 16 16:13:49 2010 +0200 @@ -33,7 +33,7 @@ let fun aux seen "" = String.implode (rev seen) | aux seen s = - if String.isPrefix bef s then + if String.isPrefix bef s then aux seen "" ^ aft ^ aux [] (unprefix bef s) else aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))