src/HOL/Tools/res_atp.ML
changeset 20854 f9cf9e62d11c
parent 20823 5480ec4b542d
child 20868 724ab9896068
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Oct 04 14:14:33 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Oct 04 14:17:38 2006 +0200
     1.3 @@ -202,12 +202,12 @@
     1.4  exception FN_LG of term;
     1.5  
     1.6  fun fn_lg (t as Const(f,tp)) (lg,seen) = 
     1.7 -    if is_hol_fn tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
     1.8 +    if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) 
     1.9    | fn_lg (t as Free(f,tp)) (lg,seen) = 
    1.10 -    if is_hol_fn tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
    1.11 +    if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) 
    1.12    | fn_lg (t as Var(f,tp)) (lg,seen) =
    1.13 -    if is_hol_fn tp then (upgrade_lg HOL lg,t ins seen) else (lg,t ins seen)
    1.14 -  | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,t ins seen)
    1.15 +    if is_hol_fn tp then (upgrade_lg HOL lg,insert (op =) t seen) else (lg,insert (op =) t seen)
    1.16 +  | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,insert (op =) t seen)
    1.17    | fn_lg f _ = raise FN_LG(f); 
    1.18  
    1.19  
    1.20 @@ -226,10 +226,10 @@
    1.21  exception PRED_LG of term;
    1.22  
    1.23  fun pred_lg (t as Const(P,tp)) (lg,seen)= 
    1.24 -      if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) 
    1.25 +      if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg,insert (op =) t seen) 
    1.26    | pred_lg (t as Free(P,tp)) (lg,seen) =
    1.27 -      if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen)
    1.28 -  | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, t ins seen)
    1.29 +      if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg,insert (op =) t seen)
    1.30 +  | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, insert (op =) t seen)
    1.31    | pred_lg P _ = raise PRED_LG(P);
    1.32  
    1.33