Merged.
authorballarin
Fri, 12 Dec 2008 15:02:15 +0100
changeset 29227 089499f104d3
parent 29226 fcc9606fe141
child 29228 40b3630b0deb
Merged.
src/HOL/ex/LocaleTest2.thy
src/Pure/Isar/subclass.ML
--- 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]