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/splitter.ML
changeset 67649 1e1782c1aedf
parent 67644 15c6256709d6
child 69593 3dda49e08b9d 
--- a/src/Provers/splitter.ML	Sat Feb 17 20:03:37 2018 +0100
+++ b/src/Provers/splitter.ML	Sun Feb 18 15:05:21 2018 +0100
@@ -440,7 +440,7 @@
     val (name, asm) = split_thm_info split
     val split0 = Thm.trim_context split
     fun tac ctxt' =
-      let val split' = Thm.transfer (Proof_Context.theory_of ctxt') split0 in
+      let val split' = Thm.transfer' ctxt' split0 in
         (if asm then split_asm_tac ctxt' [split']
          else if bang
               then split_tac ctxt' [split'] THEN_ALL_NEW
isabelle