src/FOLP/hypsubst.ML
changeset 2728 df3a269b6f34
parent 1459 d12da312eff4
child 3537 79ac9b475621
equal deleted 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