--- 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 =>
--- 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 (_, []) = []
--- 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;
--- 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;