1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Jul 29 09:41:49 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Jul 29 09:47:23 2010 +0200
     1.3 @@ -66,8 +66,7 @@
     1.4    | mk_anot phi = AConn (ANot, [phi])
     1.5  fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
     1.6  
     1.7 -val index_in_shape : int -> int list list -> int =
     1.8 -  find_index o exists o curry (op =)
     1.9 +fun index_in_shape x = find_index (exists (curry (op =) x))
    1.10  fun is_axiom_clause_number thm_names num =
    1.11    num > 0 andalso num <= Vector.length thm_names andalso
    1.12    Vector.sub (thm_names, num - 1) <> ""
    1.13 @@ -133,7 +132,8 @@
    1.14     which can be hard to disambiguate from function application in an LL(1)
    1.15     parser. As a workaround, we extend the TPTP term syntax with such detritus
    1.16     and ignore it. *)
    1.17 -val parse_vampire_detritus = scan_integer |-- $$ ":" --| scan_integer >> K []
    1.18 +fun parse_vampire_detritus x =
    1.19 +  (scan_integer |-- $$ ":" --| scan_integer >> K []) x
    1.20  
    1.21  fun parse_term pool x =
    1.22    ((scan_dollar_name >> repair_name pool)