Now uses eta_contract_atom for greater speed
authorpaulson
Wed Mar 05 10:08:32 1997 +0100 (1997-03-05 ago)
changeset 2728df3a269b6f34
parent 2727 230f2643107e
child 2729 44cbfeebd0fe
Now uses eta_contract_atom for greater speed
src/FOLP/hypsubst.ML
     1.1 --- a/src/FOLP/hypsubst.ML	Wed Mar 05 10:07:04 1997 +0100
     1.2 +++ b/src/FOLP/hypsubst.ML	Wed Mar 05 10:08:32 1997 +0100
     1.3 @@ -42,7 +42,7 @@
     1.4    It's not safe to substitute for a variable free in the premises,
     1.5      but how could we check for this?*)
     1.6  fun inspect_pair bnd (t,u) =
     1.7 -  case (Pattern.eta_contract t, Pattern.eta_contract u) of
     1.8 +  case (Pattern.eta_contract_atom t, Pattern.eta_contract_atom u) of
     1.9         (Bound i, _) => if loose(i,u) then raise Match 
    1.10                         else sym         (*eliminates t*)
    1.11       | (_, Bound i) => if loose(i,t) then raise Match