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/Tools/cong_tac.ML
changeset 59621 291934bac95e
parent 58956 a816aa3ff391
child 59642 929984c529d3 
--- a/src/Tools/cong_tac.ML	Fri Mar 06 14:01:08 2015 +0100
+++ b/src/Tools/cong_tac.ML	Fri Mar 06 15:58:56 2015 +0100
@@ -14,7 +14,7 @@
 
 fun cong_tac ctxt cong = CSUBGOAL (fn (cgoal, i) =>
   let
-    val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
+    val cert = Thm.global_cterm_of (Thm.theory_of_cterm cgoal);
     val goal = Thm.term_of cgoal;
   in
     (case Logic.strip_assums_concl goal of
isabelle