# 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;