src/Pure/display.ML
changeset 18980 fd6b42e6bf50
parent 18936 647528660980
child 19300 7689f81f8996
     1.1 --- a/src/Pure/display.ML	Wed Feb 08 15:17:54 2006 +0100
     1.2 +++ b/src/Pure/display.ML	Wed Feb 08 17:15:27 2006 +0100
     1.3 @@ -238,32 +238,30 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun ins_entry (x, y) [] = [(x, [y])]
     1.8 -  | ins_entry (x, y) ((pair as (x', ys')) :: pairs) =
     1.9 -      if x = x' then (x', y ins ys') :: pairs
    1.10 -      else pair :: ins_entry (x, y) pairs;
    1.11 +fun ins_entry (x, y) =
    1.12 +  AList.default (op =) (x, []) #>
    1.13 +  AList.map_entry (op =) x (insert (op =) y);
    1.14  
    1.15 -fun add_consts (Const (c, T), env) = ins_entry (T, (c, T)) env
    1.16 -  | add_consts (t $ u, env) = add_consts (u, add_consts (t, env))
    1.17 -  | add_consts (Abs (_, _, t), env) = add_consts (t, env)
    1.18 -  | add_consts (_, env) = env;
    1.19 +val add_consts = Term.fold_aterms
    1.20 +  (fn Const (c, T) => ins_entry (T, (c, T))
    1.21 +    | _ => I);
    1.22  
    1.23 -fun add_vars (Free (x, T), env) = ins_entry (T, (x, ~1)) env
    1.24 -  | add_vars (Var (xi, T), env) = ins_entry (T, xi) env
    1.25 -  | add_vars (Abs (_, _, t), env) = add_vars (t, env)
    1.26 -  | add_vars (t $ u, env) = add_vars (u, add_vars (t, env))
    1.27 -  | add_vars (_, env) = env;
    1.28 +val add_vars = Term.fold_aterms
    1.29 +  (fn Free (x, T) => ins_entry (T, (x, ~1))
    1.30 +    | Var (xi, T) => ins_entry (T, xi)
    1.31 +    | _ => I);
    1.32  
    1.33 -fun add_varsT (Type (_, Ts), env) = foldr add_varsT env Ts
    1.34 -  | add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env
    1.35 -  | add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env;
    1.36 +val add_varsT = Term.fold_atyps
    1.37 +  (fn TFree (x, S) => ins_entry (S, (x, ~1))
    1.38 +    | TVar (xi, S) => ins_entry (S, xi)
    1.39 +    | _ => I);
    1.40  
    1.41  fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
    1.42  fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
    1.43  
    1.44 -fun consts_of t = sort_cnsts (add_consts (t, []));
    1.45 -fun vars_of t = sort_idxs (add_vars (t, []));
    1.46 -fun varsT_of t = rev (sort_idxs (it_term_types add_varsT (t, [])));
    1.47 +fun consts_of t = sort_cnsts (add_consts t []);
    1.48 +fun vars_of t = sort_idxs (add_vars t []);
    1.49 +fun varsT_of t = rev (sort_idxs (Term.fold_types add_varsT t []));
    1.50  
    1.51  in
    1.52