src/Pure/Isar/class_declaration.ML
changeset 38390 cb72d89bb444
parent 38389 d7d915bae307
child 38435 1e1ef69ec0de
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Thu Aug 12 13:28:18 2010 +0200
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Thu Aug 12 13:42:12 2010 +0200
     1.3 @@ -311,8 +311,8 @@
     1.4      val thy = ProofContext.theory_of lthy;
     1.5      val proto_sup = prep_class thy raw_sup;
     1.6      val proto_sub = case Named_Target.peek lthy
     1.7 -     of {is_class = false, ...} => error "Not in a class context"
     1.8 -      | {target, ...} => target;
     1.9 +     of SOME {target, is_class = true, ...} => target
    1.10 +      | _ => error "Not in a class target";
    1.11      val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup);
    1.12  
    1.13      val expr = ([(sup, (("", false), Expression.Positional []))], []);