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/Decision_Procs/ferrack_tac.ML
changeset 58956 a816aa3ff391
parent 56245 84fc7dfa3cd4
child 58963 26bf09b95dda 
--- a/src/HOL/Decision_Procs/ferrack_tac.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -47,7 +47,7 @@
 
 fun linr_tac ctxt q =
     Object_Logic.atomize_prems_tac ctxt
-        THEN' (REPEAT_DETERM o split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}])
+        THEN' (REPEAT_DETERM o split_tac ctxt [@{thm split_min}, @{thm split_max}, @{thm abs_split}])
         THEN' SUBGOAL (fn (g, i) =>
   let
     val thy = Proof_Context.theory_of ctxt
isabelle