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