changeset 55169 | fda77499eef5 |
parent 55168 | 948e8b7ea82f |
child 55183 | 17ec4a29ef71 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Jan 29 22:34:34 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Jan 29 23:24:34 2014 +0100 @@ -290,8 +290,7 @@ end |> HOLogic.mk_Trueprop |> close_form - fun maybe_show outer c = - (outer andalso length c = 1 andalso subset (op =) (c, conjs)) ? cons Show + fun maybe_show outer c = (outer andalso eq_set (op =) (c, conjs)) ? cons Show fun isar_steps outer predecessor accum [] = accum