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/HOL/Nominal/nominal_thmdecls.ML
changeset 56491 a8ccf3d6a6e4
parent 56245 84fc7dfa3cd4
child 59582 0fbed69ff081 
--- a/src/HOL/Nominal/nominal_thmdecls.ML	Wed Apr 09 11:32:41 2014 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Wed Apr 09 12:22:57 2014 +0200
@@ -47,7 +47,7 @@
 
 fun tactic ctxt (msg, tac) =
   if Config.get ctxt nominal_eqvt_debug
-  then tac THEN' (K (print_tac ("after " ^ msg)))
+  then tac THEN' (K (print_tac ctxt ("after " ^ msg)))
   else tac
 
 fun prove_eqvt_tac ctxt orig_thm pi pi' =
isabelle