changeset 7645 | c67115c0e105 |
parent 6969 | 441393b452c7 |
child 13105 | 3d1e7a199bdc |
--- a/src/FOLP/simp.ML Wed Sep 29 14:34:01 1999 +0200 +++ b/src/FOLP/simp.ML Wed Sep 29 14:35:18 1999 +0200 @@ -600,7 +600,7 @@ fun mk_typed_congs thy = let val sg = sign_of thy; - val S0 = Type.defaultS(#tsig(Sign.rep_sg sg)) + val S0 = Sign.defaultS sg; fun readfT(f,s) = let val T = incr_tvar 9 (Sign.read_typ(sg,K(Some(S0))) s); val t = case Sign.const_type sg f of