Sign.defaultS;
authorwenzelm
Wed Sep 29 14:35:18 1999 +0200 (1999-09-29)
changeset 7645c67115c0e105
parent 7644 054ecaf3ca22
child 7646 1ad3866b86cc
Sign.defaultS;
src/FOLP/simp.ML
src/Provers/simp.ML
     1.1 --- a/src/FOLP/simp.ML	Wed Sep 29 14:34:01 1999 +0200
     1.2 +++ b/src/FOLP/simp.ML	Wed Sep 29 14:35:18 1999 +0200
     1.3 @@ -600,7 +600,7 @@
     1.4  
     1.5  fun mk_typed_congs thy =
     1.6  let val sg = sign_of thy;
     1.7 -    val S0 = Type.defaultS(#tsig(Sign.rep_sg sg))
     1.8 +    val S0 = Sign.defaultS sg;
     1.9      fun readfT(f,s) =
    1.10          let val T = incr_tvar 9 (Sign.read_typ(sg,K(Some(S0))) s);
    1.11              val t = case Sign.const_type sg f of
     2.1 --- a/src/Provers/simp.ML	Wed Sep 29 14:34:01 1999 +0200
     2.2 +++ b/src/Provers/simp.ML	Wed Sep 29 14:35:18 1999 +0200
     2.3 @@ -626,7 +626,7 @@
     2.4  
     2.5  fun mk_typed_congs thy =
     2.6  let val sg = sign_of thy;
     2.7 -    val S0 = Type.defaultS(#tsig(Sign.rep_sg sg))
     2.8 +    val S0 = Sign.defaultS sg;
     2.9      fun readfT(f,s) =
    2.10  	let val T = incr_tvar 9 (Sign.read_typ(sg,K(Some(S0))) s);
    2.11  	    val t = case Sign.const_type sg f of