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 42793 88bee9f6eec7
parent 42483 39eefaef816a
child 46217 7b19666f0e3d 
--- a/src/HOL/Tools/Function/function_core.ML	Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Fri May 13 22:55:00 2011 +0200
@@ -702,7 +702,7 @@
     Goal.init goal
     |> (SINGLE (resolve_tac [accI] 1)) |> the
     |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1))  |> the
-    |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the
+    |> (SINGLE (auto_tac ctxt)) |> the
     |> Goal.conclude
     |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   end
isabelle