Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Provers/eqsubst.ML
changeset 22578 b0eb5652f210
parent 21879 a3efbae45735
child 22727 473c7f67c64f 
--- a/src/Provers/eqsubst.ML	Wed Apr 04 00:10:59 2007 +0200
+++ b/src/Provers/eqsubst.ML	Wed Apr 04 00:11:03 2007 +0200
@@ -338,7 +338,7 @@
       val th = Thm.incr_indexes 1 gth;
       val tgt_term = Thm.prop_of th;
 
-      val sgn = Thm.sign_of_thm th;
+      val sgn = Thm.theory_of_thm th;
       val ctermify = Thm.cterm_of sgn;
       val trivify = Thm.trivial o ctermify;
 
@@ -448,7 +448,7 @@
       val th = Thm.incr_indexes 1 gth;
       val tgt_term = Thm.prop_of th;
 
-      val sgn = Thm.sign_of_thm th;
+      val sgn = Thm.theory_of_thm th;
       val ctermify = Thm.cterm_of sgn;
       val trivify = Thm.trivial o ctermify;
isabelle