Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
adapted Sign.infer_types;
authorwenzelm
Tue, 07 Feb 2006 19:56:56 +0100
changeset 18972 2905d1805e1e
parent 18971 f95650f3b5bf
child 18973 f88976608aad
adapted Sign.infer_types;
TFL/tfl.ML file | annotate | diff | comparison | revisions
src/HOLCF/domain/theorems.ML file | annotate | diff | comparison | revisions 
--- 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;
 
--- 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
isabelle