# HG changeset patch
# User wenzelm
# Date 880027160 -3600
# Node ID d5ccc8321e1e341b92779ffab89c09d4a5eab3d4
# Parent  f6bd8332eb3281fd5bd6a08044178dd7404fb562
tuned infer_types interface;

diff -r f6bd8332eb32 -r d5ccc8321e1e TFL/tfl.sml
--- a/TFL/tfl.sml	Thu Nov 20 12:51:55 1997 +0100
+++ b/TFL/tfl.sml	Thu Nov 20 12:59:20 1997 +0100
@@ -335,7 +335,7 @@
      val wfrec_R_M =  map_term_types poly_tvars 
 	                  (wfrec $ map_term_types poly_tvars R) 
 	              $ functional
-     val (_, def_term, _) = 
+     val (def_term, _) = 
 	 Sign.infer_types (sign_of thy) (K None) (K None) [] false
 	       ([Const("==",dummyT) $ Const(Name,Ty) $ wfrec_R_M], 
 		propT)
diff -r f6bd8332eb32 -r d5ccc8321e1e src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Thu Nov 20 12:51:55 1997 +0100
+++ b/src/HOLCF/domain/theorems.ML	Thu Nov 20 12:59:20 1997 +0100
@@ -18,7 +18,7 @@
 
 (* ----- general proof facilities ------------------------------------------- *)
 
-fun inferT sg pre_tm = #2 (Sign.infer_types sg (K None) (K None) [] true 
+fun inferT sg pre_tm = #1 (Sign.infer_types sg (K None) (K None) [] true 
                            ([pre_tm],propT));
 
 fun pg'' thy defs t = let val sg = sign_of thy;