src/Pure/Isar/class_declaration.ML

       (Const o apsnd (map_atyps (K aT))) param_map;
     val const_morph = Element.inst_morphism thy
       (Symtab.empty, Symtab.make param_map_inst);
     val typ_morph = Element.inst_morphism thy
       (Symtab.empty |> Symtab.update (Name.aT, TFree (Name.aT, [class])), Symtab.empty);
-    val (([raw_props], [(_, raw_inst_morph)], export_morph), _) = empty_ctxt
+    val (([raw_props], _, [(_, raw_inst_morph)], _, export_morph), _) = empty_ctxt
       |> Expression.cert_goal_expression ([(class, (("", false),
-           Expression.Named param_map_const))], []);
+           (Expression.Named param_map_const, [])))], []);
     val (props, inst_morph) =
       if null param_map
       then (raw_props |> map (Morphism.term typ_morph),
         raw_inst_morph $> typ_morph)
       else (raw_props, raw_inst_morph); (*FIXME proper handling in

         SOME T => map (subst_TVars (map (rpair T) param_namesT)) ts
       end;
 
     (* preprocessing elements, retrieving base sort from type-checked elements *)
     val raw_supexpr =
-      (map (fn sup => (sup, (("", false), Expression.Positional []))) sups, []);
+      (map (fn sup => (sup, (("", false), (Expression.Positional [], [])))) sups, []);
     val init_class_body =
       fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
       #> Class.redeclare_operations thy sups
       #> Context.proof_map (Syntax_Phases.term_check 0 "singleton_fixate" (K singleton_fixate));
     val ((raw_supparams, _, raw_inferred_elems, _), _) =

     val supparams = map (fn ((c, T), _) =>
       (c, map_atyps (K (TFree (Name.aT, base_sort))) T)) raw_supparams;
     val supparam_names = map fst supparams;
     fun mk_param ((c, _), _) = Free (c, (the o AList.lookup (op =) supparams) c);
     val supexpr = (map (fn sup => (sup, (("", false),
-      Expression.Positional (map (SOME o mk_param) (Locale.params_of thy sup))))) sups,
+      (Expression.Positional (map (SOME o mk_param) (Locale.params_of thy sup)), [])))) sups,
         map (fn (c, T) => (Binding.name c, SOME T, NoSyn)) supparams);
 
   in (base_sort, supparam_names, supexpr, inferred_elems) end;
 
 val cert_class_elems = prep_class_elems Expression.cert_declaration;

       (case Named_Target.class_of lthy of
         SOME class => class
       | NONE => error "Not in a class target");
     val (sub, sup) = Axclass.cert_classrel thy (proto_sub, proto_sup);
 
-    val expr = ([(sup, (("", false), Expression.Positional []))], []);
-    val (([props], deps, export), goal_ctxt) =
+    val expr = ([(sup, (("", false), (Expression.Positional [], [])))], []);
+    val (([props], _, deps, _, export), goal_ctxt) =
       Expression.cert_goal_expression expr lthy;
     val some_prop = try the_single props;
     val some_dep_morph = try the_single (map snd deps);
     fun after_qed some_wit =
       Class.register_subclass (sub, sup) some_dep_morph some_wit export;