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.
Sign.defaultS;
authorwenzelm
Wed, 29 Sep 1999 14:35:18 +0200
changeset 7645 c67115c0e105
parent 7644 054ecaf3ca22
child 7646 1ad3866b86cc
Sign.defaultS;
src/FOLP/simp.ML file | annotate | diff | comparison | revisions
src/Provers/simp.ML file | annotate | diff | comparison | revisions 
--- a/src/FOLP/simp.ML	Wed Sep 29 14:34:01 1999 +0200
+++ b/src/FOLP/simp.ML	Wed Sep 29 14:35:18 1999 +0200
@@ -600,7 +600,7 @@
 
 fun mk_typed_congs thy =
 let val sg = sign_of thy;
-    val S0 = Type.defaultS(#tsig(Sign.rep_sg sg))
+    val S0 = Sign.defaultS sg;
     fun readfT(f,s) =
         let val T = incr_tvar 9 (Sign.read_typ(sg,K(Some(S0))) s);
             val t = case Sign.const_type sg f of
--- a/src/Provers/simp.ML	Wed Sep 29 14:34:01 1999 +0200
+++ b/src/Provers/simp.ML	Wed Sep 29 14:35:18 1999 +0200
@@ -626,7 +626,7 @@
 
 fun mk_typed_congs thy =
 let val sg = sign_of thy;
-    val S0 = Type.defaultS(#tsig(Sign.rep_sg sg))
+    val S0 = Sign.defaultS sg;
     fun readfT(f,s) =
 	let val T = incr_tvar 9 (Sign.read_typ(sg,K(Some(S0))) s);
 	    val t = case Sign.const_type sg f of
isabelle