1.1 --- a/src/HOL/ex/LocaleTest2.thy	Fri Dec 12 14:26:35 2008 +0100
     1.2 +++ b/src/HOL/ex/LocaleTest2.thy	Fri Dec 12 15:02:15 2008 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/ex/LocaleTest2.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Clemens Ballarin
     1.7      Copyright (c) 2007 by Clemens Ballarin
     1.8  

     2.1 --- a/src/Pure/Isar/subclass.ML	Fri Dec 12 14:26:35 2008 +0100
     2.2 +++ b/src/Pure/Isar/subclass.ML	Fri Dec 12 15:02:15 2008 +0100
     2.3 @@ -1,5 +1,4 @@
     2.4  (*  Title:      Pure/Isar/subclass.ML
     2.5 -    ID:         $Id$
     2.6      Author:     Florian Haftmann, TU Muenchen
     2.7  
     2.8  User interface for proving subclass relationship between type classes.
     2.9 @@ -22,7 +21,7 @@
    2.10      val thy = ProofContext.theory_of lthy;
    2.11      val sup = prep_class thy raw_sup;
    2.12      val sub = case TheoryTarget.peek lthy
    2.13 -     of {is_class = false, ...} => error "No class context"
    2.14 +     of {is_class = false, ...} => error "Not a class context"
    2.15        | {target, ...} => target;
    2.16      val _ = if Sign.subsort thy ([sup], [sub])
    2.17        then error ("Class " ^ Syntax.string_of_sort lthy [sup]