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/Library/refute.ML
changeset 58322 f13f6e27d68e
parent 58129 3ec65a7f2b50
child 58354 04ac60da613e 
--- a/src/HOL/Library/refute.ML	Thu Sep 11 21:11:03 2014 +0200
+++ b/src/HOL/Library/refute.ML	Fri Sep 12 11:16:47 2014 +0200
@@ -1947,7 +1947,7 @@
                             ^ Syntax.string_of_typ ctxt (Type (s', Ts'))
                             ^ ") is not a variable")
                         else ()
-                      (* split the constructors into those occuring before/after *)
+                      (* split the constructors into those occurring before/after *)
                       (* 'Const (s, T)'                                          *)
                       val (constrs1, constrs2) = take_prefix (fn (cname, ctypes) =>
                         not (cname = s andalso Sign.typ_instance thy (T,
isabelle