src/Pure/Isar/class_target.ML

   arities: string list * (string * sort) list * sort,
   params: ((string * string) * (string * typ)) list
     (*(instantiation parameter, type constructor), (local instantiation parameter, typ)*)
 }
 
-structure Instantiation = ProofDataFun
+structure Instantiation = Proof_Data
 (
   type T = instantiation
   fun init _ = Instantiation { arities = ([], [], []), params = [] };
 );