Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 60945 88aaecbaf61e
parent 60943 7cf1ea00a020
child 60948 b710a5087116 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sun Aug 16 11:55:21 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sun Aug 16 14:48:37 2015 +0200
@@ -313,7 +313,7 @@
 
         val {safeIs, (* safeEs, *) unsafeIs, (* unsafeEs, *) ...} =
           ctxt |> claset_of |> Classical.rep_cs
-        val intros = Item_Net.content safeIs @ Item_Net.content unsafeIs
+        val intros = map #1 (Item_Net.content safeIs @ Item_Net.content unsafeIs)
 (* Add once it is used:
         val elims = Item_Net.content safeEs @ Item_Net.content unsafeEs
           |> map Classical.classical_rule
isabelle