Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Mutabelle/mutabelle_extra.ML
changeset 81363 fec95447c5bd
parent 81362 f586fdabe670
child 82364 5af097d05e99 
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Oct 22 17:31:54 2024 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Oct 24 11:37:41 2024 +0200
@@ -148,7 +148,7 @@
   let
     val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy)
   in
-    case Try0.try0 (SOME (seconds 5.0)) ([], [], [], []) state of
+    case Try0.try0 (SOME (seconds 5.0)) [] state of
       [] => (Unsolved, [])
     | _ => (Solved, [])
   end
isabelle