src/HOLCF/domain/theorems.ML
changeset 14820 3f80d6510ee9
parent 13454 01e2496dee05
child 14981 e73f8140af78
     1.1 --- a/src/HOLCF/domain/theorems.ML	Sat May 29 14:58:44 2004 +0200
     1.2 +++ b/src/HOLCF/domain/theorems.ML	Sat May 29 14:59:24 2004 +0200
     1.3 @@ -18,8 +18,8 @@
     1.4  
     1.5  (* ----- general proof facilities ------------------------------------------- *)
     1.6  
     1.7 -fun inferT sg pre_tm = #1 (Sign.infer_types sg (K None) (K None) [] true 
     1.8 -                           ([pre_tm],propT));
     1.9 +fun inferT sg pre_tm =
    1.10 +  #1 (Sign.infer_types (Sign.pp sg) sg (K None) (K None) [] true ([pre_tm],propT));
    1.11  
    1.12  fun pg'' thy defs t = let val sg = sign_of thy;
    1.13                            val ct = Thm.cterm_of sg (inferT sg t);