# HG changeset patch
# User blanchet
# Date 1280389643 -7200
# Node ID 9cb8f5432dfcad303df790bf3dd18fbdc8bee721
# Parent  9069e1ad15272ada410182926c8892db891625e9
kill polymorphic "val"s

diff -r 9069e1ad1527 -r 9cb8f5432dfc src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Jul 29 09:41:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Jul 29 09:47:23 2010 +0200
@@ -66,8 +66,7 @@
   | mk_anot phi = AConn (ANot, [phi])
 fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
 
-val index_in_shape : int -> int list list -> int =
-  find_index o exists o curry (op =)
+fun index_in_shape x = find_index (exists (curry (op =) x))
 fun is_axiom_clause_number thm_names num =
   num > 0 andalso num <= Vector.length thm_names andalso
   Vector.sub (thm_names, num - 1) <> ""
@@ -133,7 +132,8 @@
    which can be hard to disambiguate from function application in an LL(1)
    parser. As a workaround, we extend the TPTP term syntax with such detritus
    and ignore it. *)
-val parse_vampire_detritus = scan_integer |-- $$ ":" --| scan_integer >> K []
+fun parse_vampire_detritus x =
+  (scan_integer |-- $$ ":" --| scan_integer >> K []) x
 
 fun parse_term pool x =
   ((scan_dollar_name >> repair_name pool)