# HG changeset patch
# User haftmann
# Date 1457467667 -3600
# Node ID 85ebb645b1a347bd39a29ef775e632df19acc496
# Parent  7a9aa69f9b388aadf5f07a8ac84a4500554d9214
provide explicit hint concering uniqueness of derivation

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 =>
diff -r 7a9aa69f9b38 -r 85ebb645b1a3 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Tue Mar 08 21:07:46 2016 +0100
+++ b/src/Pure/sorts.ML	Tue Mar 08 21:07:47 2016 +0100
@@ -55,7 +55,7 @@
   val meet_sort_typ: algebra -> typ * sort -> typ -> typ   (*exception CLASS_ERROR*)
   val of_sort: algebra -> typ * sort -> bool
   val of_sort_derivation: algebra ->
-    {class_relation: typ -> 'a * class -> class -> 'a,
+    {class_relation: typ -> bool -> 'a * class -> class -> 'a,
      type_constructor: string * typ list -> ('a * class) list list -> class -> 'a,
      type_variable: typ -> ('a * class) list} ->
     typ * sort -> 'a list   (*exception CLASS_ERROR*)
@@ -403,9 +403,10 @@
         if S1 = S2 then map fst D1
         else
           S2 |> map (fn c2 =>
-            (case D1 |> find_first (fn (_, c1) => class_le algebra (c1, c2)) of
-              SOME d1 => class_relation T d1 c2
-            | NONE => raise CLASS_ERROR (No_Subsort (S1, S2))))
+            (case D1 |> filter (fn (_, c1) => class_le algebra (c1, c2)) of
+              [d1] => class_relation T true d1 c2
+            | (d1 :: _ :: _) => class_relation T false d1 c2
+            | [] => raise CLASS_ERROR (No_Subsort (S1, S2))))
       end;
 
     fun derive (_, []) = []
diff -r 7a9aa69f9b38 -r 85ebb645b1a3 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Tue Mar 08 21:07:46 2016 +0100
+++ b/src/Tools/Code/code_preproc.ML	Tue Mar 08 21:07:47 2016 +0100
@@ -476,7 +476,7 @@
 fun dicts_of ctxt (proj_sort, algebra) (T, sort) =
   let
     val thy = Proof_Context.theory_of ctxt;
-    fun class_relation (x, _) _ = x;
+    fun class_relation _ (x, _) _ = x;
     fun type_constructor (tyco, _) xs class =
       inst_params thy tyco (Sorts.complete_sort algebra [class])
         @ (maps o maps) fst xs;
diff -r 7a9aa69f9b38 -r 85ebb645b1a3 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Tue Mar 08 21:07:46 2016 +0100
+++ b/src/Tools/Code/code_thingol.ML	Tue Mar 08 21:07:47 2016 +0100
@@ -482,7 +482,7 @@
         val sort' = proj_sort sort;
       in map_index (fn (n, class) => (Weakening ([], Local (v, (n, sort'))), class)) sort' end;
     val typarg_witnesses = Sorts.of_sort_derivation algebra
-      {class_relation = K (Sorts.classrel_derivation algebra class_relation),
+      {class_relation = fn _ => fn _ => Sorts.classrel_derivation algebra class_relation,
        type_constructor = type_constructor,
        type_variable = type_variable} (ty, proj_sort sort)
       handle Sorts.CLASS_ERROR e => not_wellsorted ctxt permissive some_thm deps ty sort e;