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/Nitpick/nitpick.ML
changeset 35181 92d857a4e5e0
parent 35177 168041f24f80
child 35183 8580ba651489 
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Sat Feb 13 15:04:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Feb 17 10:28:04 2010 +0100
@@ -247,7 +247,7 @@
                 (if i <> 1 orelse n <> 1 then
                    "subgoal " ^ string_of_int i ^ " of " ^ string_of_int n
                  else
-                   "goal")) [orig_t]))
+                   "goal")) [Logic.list_implies (orig_assm_ts, orig_t)]))
     val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
                 else orig_t
     val assms_t = if assms orelse auto then
isabelle