# HG changeset patch # User wenzelm # Date 1246912860 -7200 # Node ID 99ac0321cd47b4a29ff56b5032cd6e6d28b9b208 # Parent d5f186aa0beda31177f79b4fb064158567da98d3 witness_sorts: proper type witnesses for hyps, not invented "'hyp" variables; diff -r d5f186aa0bed -r 99ac0321cd47 src/Pure/sign.ML --- a/src/Pure/sign.ML Mon Jul 06 21:24:30 2009 +0200 +++ b/src/Pure/sign.ML Mon Jul 06 22:41:00 2009 +0200 @@ -27,7 +27,7 @@ val defaultS: theory -> sort val subsort: theory -> sort * sort -> bool val of_sort: theory -> typ * sort -> bool - val witness_sorts: theory -> sort list -> sort list -> (typ * sort) list + val witness_sorts: theory -> (typ * sort) list -> sort list -> (typ * sort) list val is_logtype: theory -> string -> bool val typ_instance: theory -> typ * typ -> bool val typ_equiv: theory -> typ * typ -> bool diff -r d5f186aa0bed -r 99ac0321cd47 src/Pure/sorts.ML --- a/src/Pure/sorts.ML Mon Jul 06 21:24:30 2009 +0200 +++ b/src/Pure/sorts.ML Mon Jul 06 22:41:00 2009 +0200 @@ -62,7 +62,7 @@ type_constructor: string -> ('a * class) list list -> class -> 'a, type_variable: typ -> ('a * class) list} -> typ * sort -> 'a list (*exception CLASS_ERROR*) - val witness_sorts: algebra -> string list -> sort list -> sort list -> (typ * sort) list + val witness_sorts: algebra -> string list -> (typ * sort) list -> sort list -> (typ * sort) list end; structure Sorts: SORTS = @@ -432,18 +432,17 @@ fun witness_sorts algebra types hyps sorts = let fun le S1 S2 = sort_le algebra (S1, S2); - fun get_solved S2 (T, S1) = if le S1 S2 then SOME (T, S2) else NONE; - fun get_hyp S2 S1 = if le S1 S2 then SOME (TFree ("'hyp", S1), S2) else NONE; + fun get S2 (T, S1) = if le S1 S2 then SOME (T, S2) else NONE; fun mg_dom t S = SOME (mg_domain algebra t S) handle CLASS_ERROR _ => NONE; fun witn_sort _ [] solved_failed = (SOME (propT, []), solved_failed) | witn_sort path S (solved, failed) = if exists (le S) failed then (NONE, (solved, failed)) else - (case get_first (get_solved S) solved of + (case get_first (get S) solved of SOME w => (SOME w, (solved, failed)) | NONE => - (case get_first (get_hyp S) hyps of + (case get_first (get S) hyps of SOME w => (SOME w, (w :: solved, failed)) | NONE => witn_types path types S (solved, failed))) diff -r d5f186aa0bed -r 99ac0321cd47 src/Pure/type.ML --- a/src/Pure/type.ML Mon Jul 06 21:24:30 2009 +0200 +++ b/src/Pure/type.ML Mon Jul 06 22:41:00 2009 +0200 @@ -27,7 +27,7 @@ val inter_sort: tsig -> sort * sort -> sort val cert_class: tsig -> class -> class val cert_sort: tsig -> sort -> sort - val witness_sorts: tsig -> sort list -> sort list -> (typ * sort) list + val witness_sorts: tsig -> (typ * sort) list -> sort list -> (typ * sort) list type mode val mode_default: mode val mode_syntax: mode