witness_sorts: proper type witnesses for hyps, not invented "'hyp" variables;
authorwenzelm
Mon Jul 06 22:41:00 2009 +0200 (2009-07-06 ago)
changeset 3194699ac0321cd47
parent 31945 d5f186aa0bed
child 31947 7daee3bed3af
witness_sorts: proper type witnesses for hyps, not invented "'hyp" variables;
src/Pure/sign.ML
src/Pure/sorts.ML
src/Pure/type.ML
     1.1 --- a/src/Pure/sign.ML	Mon Jul 06 21:24:30 2009 +0200
     1.2 +++ b/src/Pure/sign.ML	Mon Jul 06 22:41:00 2009 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4    val defaultS: theory -> sort
     1.5    val subsort: theory -> sort * sort -> bool
     1.6    val of_sort: theory -> typ * sort -> bool
     1.7 -  val witness_sorts: theory -> sort list -> sort list -> (typ * sort) list
     1.8 +  val witness_sorts: theory -> (typ * sort) list -> sort list -> (typ * sort) list
     1.9    val is_logtype: theory -> string -> bool
    1.10    val typ_instance: theory -> typ * typ -> bool
    1.11    val typ_equiv: theory -> typ * typ -> bool
     2.1 --- a/src/Pure/sorts.ML	Mon Jul 06 21:24:30 2009 +0200
     2.2 +++ b/src/Pure/sorts.ML	Mon Jul 06 22:41:00 2009 +0200
     2.3 @@ -62,7 +62,7 @@
     2.4       type_constructor: string -> ('a * class) list list -> class -> 'a,
     2.5       type_variable: typ -> ('a * class) list} ->
     2.6      typ * sort -> 'a list   (*exception CLASS_ERROR*)
     2.7 -  val witness_sorts: algebra -> string list -> sort list -> sort list -> (typ * sort) list
     2.8 +  val witness_sorts: algebra -> string list -> (typ * sort) list -> sort list -> (typ * sort) list
     2.9  end;
    2.10  
    2.11  structure Sorts: SORTS =
    2.12 @@ -432,18 +432,17 @@
    2.13  fun witness_sorts algebra types hyps sorts =
    2.14    let
    2.15      fun le S1 S2 = sort_le algebra (S1, S2);
    2.16 -    fun get_solved S2 (T, S1) = if le S1 S2 then SOME (T, S2) else NONE;
    2.17 -    fun get_hyp S2 S1 = if le S1 S2 then SOME (TFree ("'hyp", S1), S2) else NONE;
    2.18 +    fun get S2 (T, S1) = if le S1 S2 then SOME (T, S2) else NONE;
    2.19      fun mg_dom t S = SOME (mg_domain algebra t S) handle CLASS_ERROR _ => NONE;
    2.20  
    2.21      fun witn_sort _ [] solved_failed = (SOME (propT, []), solved_failed)
    2.22        | witn_sort path S (solved, failed) =
    2.23            if exists (le S) failed then (NONE, (solved, failed))
    2.24            else
    2.25 -            (case get_first (get_solved S) solved of
    2.26 +            (case get_first (get S) solved of
    2.27                SOME w => (SOME w, (solved, failed))
    2.28              | NONE =>
    2.29 -                (case get_first (get_hyp S) hyps of
    2.30 +                (case get_first (get S) hyps of
    2.31                    SOME w => (SOME w, (w :: solved, failed))
    2.32                  | NONE => witn_types path types S (solved, failed)))
    2.33  
     3.1 --- a/src/Pure/type.ML	Mon Jul 06 21:24:30 2009 +0200
     3.2 +++ b/src/Pure/type.ML	Mon Jul 06 22:41:00 2009 +0200
     3.3 @@ -27,7 +27,7 @@
     3.4    val inter_sort: tsig -> sort * sort -> sort
     3.5    val cert_class: tsig -> class -> class
     3.6    val cert_sort: tsig -> sort -> sort
     3.7 -  val witness_sorts: tsig -> sort list -> sort list -> (typ * sort) list
     3.8 +  val witness_sorts: tsig -> (typ * sort) list -> sort list -> (typ * sort) list
     3.9    type mode
    3.10    val mode_default: mode
    3.11    val mode_syntax: mode