src/Pure/term.ML
changeset 24982 f2f0722675b1
parent 24850 0cfd722ab579
child 25050 0dc445970b4b
     1.1 --- a/src/Pure/term.ML	Thu Oct 11 19:10:23 2007 +0200
     1.2 +++ b/src/Pure/term.ML	Thu Oct 11 19:10:24 2007 +0200
     1.3 @@ -162,7 +162,6 @@
     1.4    val add_tfrees: term -> (string * sort) list -> (string * sort) list
     1.5    val add_frees: term -> (string * typ) list -> (string * typ) list
     1.6    val hidden_polymorphism: term -> typ -> (indexname * sort) list
     1.7 -  val equiv_types: term * term -> bool
     1.8    val strip_abs_eta: int -> term -> (string * typ) list * term
     1.9    val fast_indexname_ord: indexname * indexname -> order
    1.10    val indexname_ord: indexname * indexname -> order
    1.11 @@ -535,29 +534,6 @@
    1.12      | (a1, a2) => a1 = a2);
    1.13  
    1.14  
    1.15 -(* equivalence up to renaming of types variables *)
    1.16 -
    1.17 -local
    1.18 -
    1.19 -val invent_names = Name.invents Name.context Name.aT;
    1.20 -
    1.21 -fun standard_types t =
    1.22 -  let
    1.23 -    val tfrees = add_tfrees t [];
    1.24 -    val tvars = add_tvars t [];
    1.25 -    val env1 = map2 (fn (a, S) => fn a' => (TFree (a, S), TFree (a', [])))
    1.26 -      tfrees (invent_names (length tfrees));
    1.27 -    val env2 = map2 (fn ((a, i), S) => fn a' => (TVar ((a, i), S), TVar ((a', 0), [])))
    1.28 -      tvars (invent_names (length tvars));
    1.29 -  in map_types (map_atyps (perhaps (AList.lookup (op =) (env1 @ env2)))) t end;
    1.30 -
    1.31 -in
    1.32 -
    1.33 -val equiv_types = op aconv o pairself standard_types;
    1.34 -
    1.35 -end;
    1.36 -
    1.37 -
    1.38  (* fast syntactic ordering -- tuned for inequalities *)
    1.39  
    1.40  fun fast_indexname_ord ((x, i), (y, j)) =