changeset 14643 | 130076a81b84 |
parent 13480 | bb72bd43c6c3 |
child 14981 | e73f8140af78 |
--- a/src/HOLCF/adm.ML Thu Apr 22 10:49:30 2004 +0200 +++ b/src/HOLCF/adm.ML Thu Apr 22 10:52:32 2004 +0200 @@ -114,7 +114,7 @@ fun inst_adm_subst_thm state i params s T subt t paths = let val {sign, maxidx, ...} = rep_thm state; val j = maxidx+1; - val {tsig, ...} = Sign.rep_sg sign; + val tsig = Sign.tsig_of sign; val parTs = map snd (rev params); val rule = lift_rule (state, i) adm_subst; val types = the o (fst (types_sorts rule));