src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 38212 a7e92239922f
parent 38209 3d1d928dce50
child 38215 1c7d7eaebdf2
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Aug 05 21:56:22 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Aug 06 10:50:52 2010 +0200
     1.3 @@ -212,8 +212,10 @@
     1.4    val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term
     1.5    val equational_fun_axioms : hol_context -> styp -> term list
     1.6    val is_equational_fun_surely_complete : hol_context -> styp -> bool
     1.7 -  val merged_type_var_table_for_terms : term list -> (sort * string) list
     1.8 -  val merge_type_vars_in_term : bool -> (sort * string) list -> term -> term
     1.9 +  val merged_type_var_table_for_terms :
    1.10 +    theory -> term list -> (sort * string) list
    1.11 +  val merge_type_vars_in_term :
    1.12 +    theory -> bool -> (sort * string) list -> term -> term
    1.13    val ground_types_in_type : hol_context -> bool -> typ -> typ list
    1.14    val ground_types_in_terms : hol_context -> bool -> term list -> typ list
    1.15  end;
    1.16 @@ -2255,21 +2257,25 @@
    1.17  
    1.18  (** Type preprocessing **)
    1.19  
    1.20 -fun merged_type_var_table_for_terms ts =
    1.21 +fun merged_type_var_table_for_terms thy ts =
    1.22    let
    1.23 -    fun add_type (TFree (s, S)) table =
    1.24 -        (case AList.lookup (op =) table S of
    1.25 -           SOME s' =>
    1.26 -           if string_ord (s', s) = LESS then AList.update (op =) (S, s') table
    1.27 -           else table
    1.28 -         | NONE => (S, s) :: table)
    1.29 -      | add_type _ table = table
    1.30 -  in fold (fold_types (fold_atyps add_type)) ts [] end
    1.31 +    fun add (s, S) table =
    1.32 +      table
    1.33 +      |> (case AList.lookup (Sign.subsort thy o swap) table S of
    1.34 +            SOME _ => I
    1.35 +          | NONE =>
    1.36 +            filter_out (fn (S', _) => Sign.subsort thy (S, S'))
    1.37 +            #> cons (S, s))
    1.38 +    val tfrees = [] |> fold Term.add_tfrees ts
    1.39 +                    |> sort (string_ord o pairself fst)
    1.40 +  in [] |> fold add tfrees |> rev end
    1.41  
    1.42 -fun merge_type_vars_in_term merge_type_vars table =
    1.43 +fun merge_type_vars_in_term thy merge_type_vars table =
    1.44    merge_type_vars
    1.45    ? map_types (map_atyps
    1.46 -        (fn TFree (_, S) => TFree (AList.lookup (op =) table S |> the, S)
    1.47 +        (fn TFree (_, S) =>
    1.48 +            TFree (table |> find_first (fn (S', _) => Sign.subsort thy (S', S))
    1.49 +                         |> the |> swap)
    1.50            | T => T))
    1.51  
    1.52  fun add_ground_types hol_ctxt binarize =