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/partial_function.ML
changeset 61844 007d3b34080f
parent 61841 4d3527b94f2a
child 62093 bd73a2279fcd 
--- a/src/HOL/Tools/Function/partial_function.ML	Mon Dec 14 10:14:19 2015 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Mon Dec 14 11:20:31 2015 +0100
@@ -93,7 +93,7 @@
        | SOME (arg, conv) =>
            let open Conv in
               if Term.is_open arg then no_tac
-              else ((DETERM o Method.NO_CONTEXT_TACTIC ctxt o Induct.cases_tac false [[SOME arg]] NONE [])
+              else ((DETERM o Induct.cases_tac ctxt false [[SOME arg]] NONE [])
                 THEN_ALL_NEW (rewrite_with_asm_tac ctxt 0)
                 THEN_ALL_NEW eresolve_tac ctxt @{thms thin_rl}
                 THEN_ALL_NEW (CONVERSION
isabelle