# HG changeset patch # User blanchet # Date 1307450322 -7200 # Node ID 6c3a2c33fc3934e4326e84183fff8e9338a6a785 # Parent 69375eaa90165f94b571f61a3bd057bef0e36b36 prioritize more relevant facts for monomorphization diff -r 69375eaa9016 -r 6c3a2c33fc39 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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)