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/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
changeset 55309 455a7f9924df
parent 55308 dc68f6fb88d2
child 55314 e0233567a8ef 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 23:38:33 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 23:44:39 2014 +0100
@@ -187,7 +187,7 @@
 
 fun forced_intermediate_preplay_outcome_of_isar_step preplay_data l =
   let
-    val meths_outcomes as (meth1, outcome1) :: _ = the (Canonical_Label_Tab.lookup preplay_data l)
+    val meths_outcomes as (_, outcome1) :: _ = the (Canonical_Label_Tab.lookup preplay_data l)
   in
     if forall (not o Lazy.is_finished o snd) meths_outcomes then
       (case Lazy.force outcome1 of
isabelle