# HG changeset patch
# User blanchet
# Date 1357138478 -3600
# Node ID f1426d48942f4f854f721c747a3d05547d85859b
# Parent  ab5b8b5c9cbe677cff96e11d89568c470ead3a4e
fixed oversensitive Skolem handling (cf. eaa540986291)

diff -r ab5b8b5c9cbe -r f1426d48942f src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Jan 02 15:44:00 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Jan 02 15:54:38 2013 +0100
@@ -669,7 +669,7 @@
         val ref_graph = atp_proof |> map_filter dep_of_step |> make_ref_graph
         val axioms = axioms_of_ref_graph ref_graph conjs
         val tainted = tainted_atoms_of_ref_graph ref_graph conjs
-        val is_skolem = can (try (apfst (apfst Name.dest_skolem)))
+        val is_skolem = can (apfst (apfst Name.dest_skolem))
         val props =
           Symtab.empty
           |> fold (fn Definition_Step _ => I (* FIXME *)