src/FOLP/hypsubst.ML
changeset 26830 7b7139f961bd
parent 3537 79ac9b475621
child 32449 696d64ed85da
equal deleted inserted replaced
26829:229e8078b1e0 26830:7b7139f961bd
    40   It's not safe to substitute for x=t[x] since x is not eliminated.
    40   It's not safe to substitute for x=t[x] since x is not eliminated.
    41   It's not safe to substitute for a Var; what if it appears in other goals?
    41   It's not safe to substitute for a Var; what if it appears in other goals?
    42   It's not safe to substitute for a variable free in the premises,
    42   It's not safe to substitute for a variable free in the premises,
    43     but how could we check for this?*)
    43     but how could we check for this?*)
    44 fun inspect_pair bnd (t,u) =
    44 fun inspect_pair bnd (t,u) =
    45   case (Pattern.eta_contract_atom t, Pattern.eta_contract_atom u) of
    45   case (Envir.eta_contract t, Envir.eta_contract u) of
    46        (Bound i, _) => if loose(i,u) then raise Match 
    46        (Bound i, _) => if loose(i,u) then raise Match 
    47                        else sym         (*eliminates t*)
    47                        else sym         (*eliminates t*)
    48      | (_, Bound i) => if loose(i,t) then raise Match 
    48      | (_, Bound i) => if loose(i,t) then raise Match 
    49                        else asm_rl      (*eliminates u*)
    49                        else asm_rl      (*eliminates u*)
    50      | (Free _, _) => if bnd orelse Logic.occs(t,u) then raise Match 
    50      | (Free _, _) => if bnd orelse Logic.occs(t,u) then raise Match