--- a/src/HOL/Tools/TFL/casesplit.ML Wed Sep 12 22:00:29 2012 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML Wed Sep 12 23:18:26 2012 +0200
@@ -7,7 +7,7 @@
signature CASE_SPLIT =
sig
(* try to recursively split conjectured thm to given list of thms *)
- val splitto : thm list -> thm -> thm
+ val splitto : Proof.context -> thm list -> thm -> thm
end;
structure CaseSplit: CASE_SPLIT =
@@ -121,7 +121,7 @@
(* Note: This should not be a separate tactic but integrated into the
case split done during recdef's case analysis, this would avoid us
having to (re)search for variables to split. *)
-fun splitto splitths genth =
+fun splitto ctxt splitths genth =
let
val _ = not (null splitths) orelse error "splitto: no given splitths";
val thy = Thm.theory_of_thm genth;
@@ -142,7 +142,7 @@
let
val gt = HOLogic.dest_Trueprop (#1 (Logic.dest_implies (Thm.prop_of th)));
val split_thm = mk_casesplit_goal_thm thy v gt;
- val (subthms, expf) = IsaND.fixed_subgoal_thms split_thm;
+ val (subthms, expf) = IsaND.fixed_subgoal_thms ctxt split_thm;
in
expf (map recsplitf subthms)
end)