tuned
authorhaftmann
Fri Jul 10 07:59:28 2009 +0200 (2009-07-10 ago)
changeset 31987f4c7be4d684f
parent 31986 a68f88d264f7
child 31988 801aabf9f376
tuned
src/Pure/Isar/class.ML
     1.1 --- a/src/Pure/Isar/class.ML	Fri Jul 10 07:59:27 2009 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Fri Jul 10 07:59:28 2009 +0200
     1.3 @@ -311,7 +311,7 @@
     1.4      val proto_sub = case TheoryTarget.peek lthy
     1.5       of {is_class = false, ...} => error "Not in a class context"
     1.6        | {target, ...} => target;
     1.7 -    val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup)
     1.8 +    val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup);
     1.9  
    1.10      val expr = ([(sup, (("", false), Expression.Positional []))], []);
    1.11      val (([props], deps, export), goal_ctxt) =