src/Pure/Tools/class_package.ML

 
 fun gen_instance mk_prop add_thm after_qed inst thy =
   thy
   |> ProofContext.init
   |> Proof.theorem_i PureThy.internalK NONE (after_qed oo (fold o fold) add_thm) NONE ("", [])
-       (map (fn t => (("", []), [(t, ([], []))])) (mk_prop thy inst));
+       (map (fn t => (("", []), [(t, [])])) (mk_prop thy inst));
 
 in
 
 val axclass_instance_subclass =
   gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) AxClass.add_classrel I;