src/HOL/Mutabelle/mutabelle_extra.ML
changeset 41999 3c029ef9e0f2
parent 41755 404d94506599
child 42012 2c3fe3cbebae
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Mar 18 17:27:28 2011 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Mar 18 22:55:28 2011 +0100
@@ -150,7 +150,7 @@
   let
     val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy)
   in
-    case Try.invoke_try (SOME (seconds 5.0)) state of
+    case Try.invoke_try (SOME (seconds 5.0)) ([], [], []) state of
       true => (Solved, ([], NONE))
     | false => (Unsolved, ([], NONE))
   end