src/Provers/hypsubst.ML
changeset 2174 0829b7b632c5
parent 2143 093bbe6d333b
child 2722 3e07c20b967c
equal deleted inserted replaced
2173:08c68550460b 2174:0829b7b632c5
    52 
    52 
    53 local open Data in
    53 local open Data in
    54 
    54 
    55 exception EQ_VAR;
    55 exception EQ_VAR;
    56 
    56 
    57 fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]);
    57 fun loose (i,t) = 0 mem_int add_loose_bnos(t,i,[]);
    58 
    58 
    59 local val odot = ord"."
    59 local val odot = ord"."
    60 in
    60 in
    61 (*Simplifier turns Bound variables to dotted Free variables: 
    61 (*Simplifier turns Bound variables to dotted Free variables: 
    62   change it back (any Bound variable will do)
    62   change it back (any Bound variable will do)