src/FOLP/simp.ML
changeset 14643 130076a81b84
parent 13105 3d1e7a199bdc
child 14772 c52060b69a8c
     1.1 --- a/src/FOLP/simp.ML	Thu Apr 22 10:49:30 2004 +0200
     1.2 +++ b/src/FOLP/simp.ML	Thu Apr 22 10:52:32 2004 +0200
     1.3 @@ -556,7 +556,7 @@
     1.4  in find subst_thms end;
     1.5  
     1.6  fun mk_cong sg (f,aTs,rT) (refl,eq) =
     1.7 -let val tsig = #tsig(Sign.rep_sg sg);
     1.8 +let val tsig = Sign.tsig_of sg;
     1.9      val k = length aTs;
    1.10      fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) =
    1.11          let val ca = cterm_of sg va
    1.12 @@ -578,7 +578,7 @@
    1.13  
    1.14  fun mk_cong_type sg (f,T) =
    1.15  let val (aTs,rT) = strip_type T;
    1.16 -    val tsig = #tsig(Sign.rep_sg sg);
    1.17 +    val tsig = Sign.tsig_of sg;
    1.18      fun find_refl(r::rs) =
    1.19          let val (Const(eq,eqT),_,_) = dest_red(concl_of r)
    1.20          in if Type.typ_instance(tsig, rT, hd(binder_types eqT))