diff -r 2bfe5de2d1fa -r 130076a81b84 src/Provers/simp.ML
--- a/src/Provers/simp.ML	Thu Apr 22 10:49:30 2004 +0200
+++ b/src/Provers/simp.ML	Thu Apr 22 10:52:32 2004 +0200
@@ -582,7 +582,7 @@
 in find subst_thms end;
 
 fun mk_cong sg (f,aTs,rT) (refl,eq) =
-let val tsig = #tsig(Sign.rep_sg sg);
+let val tsig = Sign.tsig_of sg;
     val k = length aTs;
     fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) =
 	let val ca = cterm_of sg va
@@ -604,7 +604,7 @@
 
 fun mk_cong_type sg (f,T) =
 let val (aTs,rT) = strip_type T;
-    val tsig = #tsig(Sign.rep_sg sg);
+    val tsig = Sign.tsig_of sg;
     fun find_refl(r::rs) =
 	let val (Const(eq,eqT),_,_) = dest_red(concl_of r)
 	in if Type.typ_instance(tsig, rT, hd(binder_types eqT))