changeset 39377 | 9e544eb396dc |
parent 39232 | 69c6d3e87660 |
child 39451 | 8893562a954b |
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Tue Sep 14 23:38:20 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Tue Sep 14 23:38:36 2010 +0200 @@ -160,7 +160,7 @@ val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt) in (case TimeLimit.timeLimit time (Seq.pull o full_tac) goal of - SOME (thm, _) => true + SOME _ => true | NONE => false) end