changeset 20074 | b4d0b545df01 |
parent 18708 | 4b3dadb4fe33 |
child 20945 | 1de0d565b483 |
--- a/src/Provers/hypsubst.ML Tue Jul 11 12:16:58 2006 +0200 +++ b/src/Provers/hypsubst.ML Tue Jul 11 12:16:59 2006 +0200 @@ -74,7 +74,7 @@ change it back (any Bound variable will do)*) fun contract t = (case Pattern.eta_contract_atom t of - Free (a, T) => if Term.is_bound a then Bound 0 else Free (a, T) + Free (a, T) => if Name.is_bound a then Bound 0 else Free (a, T) | t' => t'); fun has_vars t = maxidx_of_term t <> ~1;