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