--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 23:20:12 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 23:38:33 2014 +0100
@@ -172,8 +172,8 @@
|> map (apsnd Lazy.value)
|> fold (fn meth => AList.default (op =) (meth, lazy_preplay meth)) meths
in
- preplay_data := Canonical_Label_Tab.map_default (l, [])
- (fold (AList.update (op =)) meths_outcomes) (!preplay_data)
+ preplay_data := Canonical_Label_Tab.update (l, fold (AList.update (op =)) meths_outcomes [])
+ (!preplay_data)
end
| set_preplay_outcomes_of_isar_step _ _ _ _ _ = ()