src/Pure/Isar/class.ML

     val tac = ALLGOALS (ProofContext.fact_tac facts);
     val prfx = class_prefix class;
   in
     thy
     |> fold_map (get_remove_global_constraint o fst o snd) params
-    ||> prove_interpretation tac ((false, prfx), []) (Locale.Locale class) (inst, defs)
+    ||> prove_interpretation tac ((false, prfx), []) (Locale.Locale class)
+          (inst, map (fn def => (("", []), def)) defs)
     |-> (fn cs => fold (Sign.add_const_constraint o apsnd SOME) cs)
   end;
 
 fun intro_classes_tac facts st =
   let