# HG changeset patch
# User wenzelm
# Date 1139338616 -3600
# Node ID 2905d1805e1e32076d05c3dde0250a9cd5ff9b71
# Parent  f95650f3b5bf3e8fce37aff9a5a564d4d1d95937
adapted Sign.infer_types;

diff -r f95650f3b5bf -r 2905d1805e1e TFL/tfl.ML
--- a/TFL/tfl.ML	Tue Feb 07 19:56:54 2006 +0100
+++ b/TFL/tfl.ML	Tue Feb 07 19:56:56 2006 +0100
@@ -368,7 +368,7 @@
 
 (*For Isabelle, the lhs of a definition must be a constant.*)
 fun mk_const_def sign (c, Ty, rhs) =
-    Sign.infer_types (Sign.pp sign) sign (K NONE) (K NONE) [] false
+    Sign.infer_types (Sign.pp sign) sign (Sign.consts_of sign) (K NONE) (K NONE) [] false
                ([Const("==",dummyT) $ Const(c,Ty) $ rhs], propT)
     |> #1;
 
diff -r f95650f3b5bf -r 2905d1805e1e src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Tue Feb 07 19:56:54 2006 +0100
+++ b/src/HOLCF/domain/theorems.ML	Tue Feb 07 19:56:56 2006 +0100
@@ -19,8 +19,9 @@
 
 (* ----- general proof facilities ------------------------------------------- *)
 
+(* FIXME better avoid this low-level stuff *)
 fun inferT sg pre_tm =
-  #1 (Sign.infer_types (Sign.pp sg) sg (K NONE) (K NONE) [] true ([pre_tm],propT));
+  #1 (Sign.infer_types (Sign.pp sg) sg (Sign.consts_of sg) (K NONE) (K NONE) [] true ([pre_tm],propT));
 
 fun pg'' thy defs t tacs =
   let val t' = inferT thy t in