changeset 231 | cb6a24451544 |
parent 0 | a5a9c433f639 |
child 646 | 7928c9760667 |
--- a/src/Provers/hypsubst.ML Tue Jan 18 15:57:40 1994 +0100 +++ b/src/Provers/hypsubst.ML Tue Jan 18 16:37:12 1994 +0100 @@ -79,7 +79,7 @@ val params = Logic.strip_params Bi val var = liftvar (maxidx+1) (map #2 params) and u = Unify.rlist_abs(rev params, t) - and cterm = Sign.cterm_of sign + and cterm = cterm_of sign in cterm_instantiate [(cterm var, cterm u)] (lift_rule (state,i) rule) end;