Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned
authorhaftmann
Fri, 10 Jul 2009 07:59:28 +0200
changeset 31987 f4c7be4d684f
parent 31986 a68f88d264f7
child 31988 801aabf9f376
tuned
src/Pure/Isar/class.ML file | annotate | diff | comparison | revisions 
--- 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