# HG changeset patch
# User wenzelm
# Date 1427568825 -3600
# Node ID 4bce61dd88d2a800acfa88d2db5cb50be6954bb8
# Parent  0e9baaf0e0bb5ede23b8455525ee2de8aa60490f
clarified goal context;

diff -r 0e9baaf0e0bb -r 4bce61dd88d2 src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Sat Mar 28 17:26:42 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML	Sat Mar 28 19:53:45 2015 +0100
@@ -15,7 +15,7 @@
     ((indexname * Position.T) * string) list -> string list -> thm -> thm
   val read_term: string -> Proof.context -> term * Proof.context
   val schematic: bool Config.T
-  val goal_context: int -> thm -> Proof.context -> (string * typ) list * Proof.context
+  val goal_context: term -> Proof.context -> (string * typ) list * Proof.context
   val res_inst_tac: Proof.context ->
     ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm ->
     int -> tactic
@@ -211,11 +211,10 @@
 
 val schematic = Attrib.setup_config_bool @{binding rule_insts_schematic} (K true);
 
-fun goal_context i st ctxt =
+fun goal_context goal ctxt =
   let
-    val goal = Thm.term_of (Thm.cprem_of st i);
     val ((_, params), ctxt') = ctxt
-      |> Thm.fold_terms Variable.declare_constraints st
+      |> Variable.declare_constraints goal
       |> Variable.improper_fixes
       |> Variable.focus_params goal
       ||> Variable.restore_proper_fixes ctxt
@@ -229,7 +228,7 @@
   let
     (* goal context *)
 
-    val (params, param_ctxt) = goal_context i st ctxt;
+    val (params, param_ctxt) = goal_context (Thm.term_of cgoal) ctxt;
     val paramTs = map #2 params;
 
 
diff -r 0e9baaf0e0bb -r 4bce61dd88d2 src/Tools/induct_tacs.ML
--- a/src/Tools/induct_tacs.ML	Sat Mar 28 17:26:42 2015 +0100
+++ b/src/Tools/induct_tacs.ML	Sat Mar 28 19:53:45 2015 +0100
@@ -26,7 +26,7 @@
         quote (Syntax.string_of_term ctxt u) ^ Position.here pos);
   in (u, U) end;
 
-fun case_tac ctxt s fixes opt_rule i st =
+fun case_tac ctxt s fixes opt_rule = SUBGOAL (fn (goal, i) =>
   let
     val rule =
       (case opt_rule of
@@ -34,7 +34,7 @@
       | NONE =>
           let
             val (t, ctxt') = ctxt
-              |> Rule_Insts.goal_context i st |> #2
+              |> Rule_Insts.goal_context goal |> #2
               |> Context_Position.set_visible false
               |> Rule_Insts.read_term s;
             val pos = Syntax.read_input_pos s;
@@ -44,13 +44,11 @@
             | [] => @{thm case_split})
           end);
     val _ = Method.trace ctxt [rule];
-
-    val xi =
-      (case Induct.vars_of (Thm.term_of (Thm.cprem_of rule 1)) of
-        Var (xi, _) :: _ => xi
-      | _ => raise THM ("Malformed cases rule", 0, [rule]));
-  in Rule_Insts.res_inst_tac ctxt [((xi, Position.none), s)] fixes rule i st end
-  handle THM _ => Seq.empty;
+  in
+    (case Induct.vars_of (Thm.term_of (Thm.cprem_of rule 1)) handle THM _ => [] of
+      Var (xi, _) :: _ => Rule_Insts.res_inst_tac ctxt [((xi, Position.none), s)] fixes rule i
+    | _ => no_tac)
+  end);
 
 
 (* induction *)