diff -r 7a9aa69f9b38 -r 85ebb645b1a3 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Mar 08 21:07:46 2016 +0100
+++ b/src/Pure/proofterm.ML	Tue Mar 08 21:07:47 2016 +0100
@@ -1057,7 +1057,7 @@
 
 fun of_sort_proof thy hyps =
   Sorts.of_sort_derivation (Sign.classes_of thy)
-   {class_relation = fn typ => fn (prf, c1) => fn c2 =>
+   {class_relation = fn typ => fn _ => fn (prf, c1) => fn c2 =>
       if c1 = c2 then prf
       else canonical_instance [typ] (classrel_proof thy (c1, c2)) %% prf,
     type_constructor = fn (a, typs) => fn dom => fn c =>