src/FOLP/hypsubst.ML
 changeset 2728 df3a269b6f34 parent 1459 d12da312eff4 child 3537 79ac9b475621
equal inserted replaced
2727:230f2643107e 2728:df3a269b6f34
`    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 t, Pattern.eta_contract u) of`
`    45   case (Pattern.eta_contract_atom t, Pattern.eta_contract_atom 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 `