src/Provers/hypsubst.ML
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;