# HG changeset patch # User blanchet # Date 1391034274 -3600 # Node ID fda77499eef5f5a9a64b5917e4b3961ed2af4533 # Parent 948e8b7ea82f0150143d49f2ab76025dcdcfa4f1 proper 'show' detection diff -r 948e8b7ea82f -r fda77499eef5 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- 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