changeset 54131 | 18b23d787062 |
parent 54125 | 420b876ff1e2 |
child 54140 | 564b8adb0952 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Oct 17 02:22:54 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Oct 17 02:29:49 2013 +0200 @@ -1188,7 +1188,7 @@ Isar_Proof => 0 | Automatic_Proof => 2 * max_isar | Isar_Proof_wegen_Prover_Flop => max_isar) - - 500 * length (isar_dependencies_of name_tabs th) + - 100 * length (isar_dependencies_of name_tabs th) val old_facts = facts |> filter is_in_access_G |> map (`priority_of)