src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML

             val num_of_constrs = length case_thms
             val (_, ts) = strip_comb t
           in
             trace_tac ctxt options ("Term " ^ (Syntax.string_of_term ctxt t) ^
               " splitting with rules \n" ^ Display.string_of_thm ctxt split_asm)
-            THEN TRY (Splitter.split_asm_tac [split_asm] 1
+            THEN TRY (Splitter.split_asm_tac ctxt [split_asm] 1
               THEN (trace_tac ctxt options "after splitting with split_asm rules")
             (* THEN (Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) 1)
               THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*)
               THEN (REPEAT_DETERM_N (num_of_constrs - 1)
                 (etac @{thm botE} 1 ORELSE etac @{thm botE} 2)))

             THEN (EVERY (map split_term_tac ts))
           end
       else all_tac
   in
     split_term_tac (HOLogic.mk_tuple out_ts)
-    THEN (DETERM (TRY ((Splitter.split_asm_tac [@{thm "split_if_asm"}] 1)
+    THEN (DETERM (TRY ((Splitter.split_asm_tac ctxt [@{thm "split_if_asm"}] 1)
     THEN (etac @{thm botE} 2))))
   end
 
 (* VERY LARGE SIMILIRATIY to function prove_param
 -- join both functions