--- a/src/Pure/Proof/proof_syntax.ML Thu May 11 19:19:31 2006 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Thu May 11 19:19:33 2006 +0200
@@ -113,7 +113,7 @@
val prop' = the_default (Bound 0) (AList.lookup (op =) thms' s);
val ps = remove (op =) prop' (map fst (the (Symtab.lookup thms s)))
in if prop = prop' then prf' else
- PThm ((s ^ "_" ^ string_of_int (length ps - find_index_eq prop ps), tags),
+ PThm ((s ^ "_" ^ string_of_int (length ps - find_index (fn p => p = prop) ps), tags),
prf, prop, Ts)
end
| rename prf = prf