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_filter.ML
changeset 42729 e011f632227c
parent 42728 44cd74a419ce
child 42730 d6db5a815477 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu May 12 15:29:19 2011 +0200
@@ -493,6 +493,7 @@
 fun pconsts_in_fact thy is_built_in_const t =
   Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
               (pconsts_in_terms thy is_built_in_const true (SOME true) [t]) []
+
 fun pair_consts_fact thy is_built_in_const fudge fact =
   case fact |> snd |> theory_const_prop_of fudge
             |> pconsts_in_fact thy is_built_in_const of
isabelle