src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
changeset 62826 eb94e570c1a4
parent 62219 dbac573b27e7
child 63097 ee8edbcbb4ad
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Sat Apr 02 23:14:08 2016 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Sat Apr 02 23:29:05 2016 +0200
     1.3 @@ -45,7 +45,7 @@
     1.4  
     1.5      fun minimize_half _ min_facts [] time = (min_facts, time)
     1.6        | minimize_half mk_step min_facts (fact :: facts) time =
     1.7 -        (case preplay_isar_step_for_method ctxt [] (Time.+ (time, slack)) meth
     1.8 +        (case preplay_isar_step_for_method ctxt [] (time + slack) meth
     1.9              (mk_step (min_facts @ facts)) of
    1.10            Played time' => minimize_half mk_step min_facts facts time'
    1.11          | _ => minimize_half mk_step (fact :: min_facts) facts time)