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/Tools/Function/function_core.ML
changeset 58963 26bf09b95dda
parent 58950 d07464875dd4
child 59498 50b60f501b05 
--- a/src/HOL/Tools/Function/function_core.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/Function/function_core.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -683,7 +683,7 @@
       subset_induct_rule
       |> Thm.forall_intr (cterm_of thy D)
       |> Thm.forall_elim (cterm_of thy acc_R)
-      |> assume_tac 1 |> Seq.hd
+      |> atac 1 |> Seq.hd
       |> (curry op COMP) (acc_downward
         |> (instantiate' [SOME (ctyp_of thy domT)]
              (map (SOME o cterm_of thy) [R, x, z]))
isabelle