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/BNF/Tools/bnf_def_tactics.ML
changeset 49586 d5e342ffe91e
parent 49510 ba50d204095e
child 49621 55cdf03e46c4 
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -106,7 +106,7 @@
 
 fun mk_srel_Id_tac n srel_Gr map_id {context = ctxt, prems = _} =
   unfold_thms_tac ctxt [srel_Gr, @{thm Id_alt}] THEN
-  subst_tac ctxt [map_id] 1 THEN
+  subst_tac ctxt NONE [map_id] 1 THEN
     (if n = 0 then rtac refl 1
     else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]},
       rtac equalityI, rtac subset_UNIV, rtac subsetI, rtac CollectI,
isabelle