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/IsaPlanner/rw_inst.ML
changeset 22578 b0eb5652f210
parent 20664 ffbc5a57191a 
--- a/src/Provers/IsaPlanner/rw_inst.ML	Wed Apr 04 00:10:59 2007 +0200
+++ b/src/Provers/IsaPlanner/rw_inst.ML	Wed Apr 04 00:11:03 2007 +0200
@@ -101,7 +101,7 @@
 (* Note, we take abstraction in the order of last abstraction first *)
 fun mk_abstractedrule TsFake Ts rule = 
     let 
-      val ctermify = Thm.cterm_of (Thm.sign_of_thm rule);
+      val ctermify = Thm.cterm_of (Thm.theory_of_thm rule);
 
       (* now we change the names of temporary free vars that represent 
          bound vars with binders outside the redex *)
@@ -225,7 +225,7 @@
 fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm = 
     let 
       (* general signature info *)
-      val target_sign = (Thm.sign_of_thm target_thm);
+      val target_sign = (Thm.theory_of_thm target_thm);
       val ctermify = Thm.cterm_of target_sign;
       val ctypeify = Thm.ctyp_of target_sign;
isabelle