changeset 28375 | c879d88d038a |
parent 28289 | efd53393412b |
child 28410 | 927e603def1f |
--- a/src/Pure/Isar/proof.ML Fri Sep 26 17:24:15 2008 +0200 +++ b/src/Pure/Isar/proof.ML Fri Sep 26 19:07:56 2008 +0200 @@ -342,7 +342,7 @@ | subgoals n = string_of_int n ^ " subgoals"; fun description strs = - (case filter_out (equal "") strs of [] => "" + (case filter_out (fn s => s = "") strs of [] => "" | strs' => enclose " (" ")" (commas strs')); fun prt_goal (SOME (ctxt, (i,