src/FOLP/hypsubst.ML
 changeset 26830 7b7139f961bd parent 3537 79ac9b475621 child 32449 696d64ed85da
equal 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 `