--- a/TFL/tfl.ML Sat May 29 14:58:44 2004 +0200
+++ b/TFL/tfl.ML Sat May 29 14:59:24 2004 +0200
@@ -371,7 +371,7 @@
(*For Isabelle, the lhs of a definition must be a constant.*)
fun mk_const_def sign (Name, Ty, rhs) =
- Sign.infer_types sign (K None) (K None) [] false
+ Sign.infer_types (Sign.pp sign) sign (K None) (K None) [] false
([Const("==",dummyT) $ Const(Name,Ty) $ rhs], propT)
|> #1;
--- 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);