# HG changeset patch
# User haftmann
# Date 1247205568 -7200
# Node ID f4c7be4d684ff7292c74c40c10930b13de3a5b06
# Parent  a68f88d264f75e57c1de5da5a2be586101403784
tuned

diff -r a68f88d264f7 -r f4c7be4d684f src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Jul 10 07:59:27 2009 +0200
+++ b/src/Pure/Isar/class.ML	Fri Jul 10 07:59:28 2009 +0200
@@ -311,7 +311,7 @@
     val proto_sub = case TheoryTarget.peek lthy
      of {is_class = false, ...} => error "Not in a class context"
       | {target, ...} => target;
-    val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup)
+    val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup);
 
     val expr = ([(sup, (("", false), Expression.Positional []))], []);
     val (([props], deps, export), goal_ctxt) =