--- 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)
--- 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;