diff -r 4dae1cb304a4 -r 3f80d6510ee9 src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Sat May 29 14:58:44 2004 +0200
+++ b/src/HOLCF/domain/theorems.ML	Sat May 29 14:59:24 2004 +0200
@@ -18,8 +18,8 @@
 
 (* ----- general proof facilities ------------------------------------------- *)
 
-fun inferT sg pre_tm = #1 (Sign.infer_types sg (K None) (K None) [] true 
-                           ([pre_tm],propT));
+fun inferT sg pre_tm =
+  #1 (Sign.infer_types (Sign.pp sg) sg (K None) (K None) [] true ([pre_tm],propT));
 
 fun pg'' thy defs t = let val sg = sign_of thy;
                           val ct = Thm.cterm_of sg (inferT sg t);