Merged.
--- a/src/HOL/ex/LocaleTest2.thy Fri Dec 12 14:26:35 2008 +0100
+++ b/src/HOL/ex/LocaleTest2.thy Fri Dec 12 15:02:15 2008 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/ex/LocaleTest2.thy
- ID: $Id$
Author: Clemens Ballarin
Copyright (c) 2007 by Clemens Ballarin
--- a/src/Pure/Isar/subclass.ML Fri Dec 12 14:26:35 2008 +0100
+++ b/src/Pure/Isar/subclass.ML Fri Dec 12 15:02:15 2008 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/subclass.ML
- ID: $Id$
Author: Florian Haftmann, TU Muenchen
User interface for proving subclass relationship between type classes.
@@ -22,7 +21,7 @@
val thy = ProofContext.theory_of lthy;
val sup = prep_class thy raw_sup;
val sub = case TheoryTarget.peek lthy
- of {is_class = false, ...} => error "No class context"
+ of {is_class = false, ...} => error "Not a class context"
| {target, ...} => target;
val _ = if Sign.subsort thy ([sup], [sub])
then error ("Class " ^ Syntax.string_of_sort lthy [sup]