Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/class.ML
changeset 31987 f4c7be4d684f
parent 31944 c8a35979a5bc
child 32113 bafffa63ebfd 
--- 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) =
isabelle