Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed oversensitive Skolem handling (cf. eaa540986291)
authorblanchet
Wed, 02 Jan 2013 15:54:38 +0100
changeset 50673 f1426d48942f
parent 50672 ab5b8b5c9cbe
child 50674 70a1c2731ab6
fixed oversensitive Skolem handling (cf. eaa540986291)
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML file | annotate | diff | comparison | revisions 
--- 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 *)
isabelle