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_provers.ML
changeset 43249 6c3a2c33fc39
parent 43248 69375eaa9016
child 43259 30c141dc22d6 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 07 14:17:35 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 07 14:38:42 2011 +0200
@@ -603,9 +603,14 @@
                 val subgoal_th =
                   Logic.list_implies (hyp_ts, concl_t)
                   |> Skip_Proof.make_thm thy
+                val rths =
+                  facts |> chop (length facts div 4)
+                        |>> map (pair 1 o snd)
+                        ||> map (pair 2 o snd)
+                        |> op @
+                        |> cons (0, subgoal_th)
               in
-                Monomorph.monomorph atp_schematic_consts_of
-                    (subgoal_th :: map snd facts |> map (pair 0)) ctxt
+                Monomorph.monomorph atp_schematic_consts_of rths ctxt
                 |> fst |> tl
                 |> curry ListPair.zip (map fst facts)
                 |> maps (fn (name, rths) => map (pair name o snd) rths)
isabelle