src/HOLCF/domain/theorems.ML
changeset 4252 d5ccc8321e1e
parent 4221 ed0f67fb458b
child 4271 3a82492e70c5
     1.1 --- a/src/HOLCF/domain/theorems.ML	Thu Nov 20 12:51:55 1997 +0100
     1.2 +++ b/src/HOLCF/domain/theorems.ML	Thu Nov 20 12:59:20 1997 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4  
     1.5  (* ----- general proof facilities ------------------------------------------- *)
     1.6  
     1.7 -fun inferT sg pre_tm = #2 (Sign.infer_types sg (K None) (K None) [] true 
     1.8 +fun inferT sg pre_tm = #1 (Sign.infer_types sg (K None) (K None) [] true 
     1.9                             ([pre_tm],propT));
    1.10  
    1.11  fun pg'' thy defs t = let val sg = sign_of thy;