src/Pure/Isar/class_declaration.ML
changeset 57182 79d43c510b84
parent 57181 2d13bf9ea77b
child 58293 1d0343818ec0
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Fri Jun 06 19:19:46 2014 +0200
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Sat Jun 07 08:16:03 2014 +0200
     1.3 @@ -346,10 +346,9 @@
     1.4    let
     1.5      val thy = Proof_Context.theory_of lthy;
     1.6      val proto_sup = prep_class thy raw_sup;
     1.7 -    val proto_sub =
     1.8 -      (case Named_Target.peek lthy of
     1.9 -         SOME {target, is_class = true, ...} => target
    1.10 -      | _ => error "Not in a class target");
    1.11 +    val proto_sub = case Named_Target.class_of lthy of
    1.12 +        SOME class => class
    1.13 +      | NONE => error "Not in a class target";
    1.14      val (sub, sup) = Axclass.cert_classrel thy (proto_sub, proto_sup);
    1.15  
    1.16      val expr = ([(sup, (("", false), Expression.Positional []))], []);