# HG changeset patch
# User wenzelm
# Date 1427570530 -3600
# Node ID 96008563bfee540dfe17ec2d70dfc0f4bf61d493
# Parent  4bce61dd88d2a800acfa88d2db5cb50be6954bb8
clarified goal context;

diff -r 4bce61dd88d2 -r 96008563bfee src/Tools/induct_tacs.ML
--- a/src/Tools/induct_tacs.ML	Sat Mar 28 19:53:45 2015 +0100
+++ b/src/Tools/induct_tacs.ML	Sat Mar 28 20:22:10 2015 +0100
@@ -64,32 +64,34 @@
 
 in
 
-fun induct_tac ctxt0 varss opt_rules i st =
+fun induct_tac ctxt varss opt_rules i st =
   let
-    val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
-    val (prems, concl) = Logic.strip_horn (Thm.term_of goal);
+    val goal = Thm.cprem_of st i;
+    val (_, goal_ctxt) = Rule_Insts.goal_context (Thm.term_of goal) ctxt
+    and ((_, goal'), _) = Variable.focus_cterm goal ctxt;
+    val (prems, concl) = Logic.strip_horn (Thm.term_of goal');
 
     fun induct_var name =
       let
-        val t = Syntax.read_term ctxt name;
+        val t = Syntax.read_term goal_ctxt name;
         val pos = Syntax.read_input_pos name;
         val (x, _) = Term.dest_Free t handle TERM _ =>
           error ("Induction argument not a variable: " ^
-            quote (Syntax.string_of_term ctxt t) ^ Position.here pos);
+            quote (Syntax.string_of_term goal_ctxt t) ^ Position.here pos);
         val eq_x = fn Free (y, _) => x = y | _ => false;
         val _ =
           if Term.exists_subterm eq_x concl then ()
           else
             error ("No such variable in subgoal: " ^
-              quote (Syntax.string_of_term ctxt t) ^ Position.here pos);
+              quote (Syntax.string_of_term goal_ctxt t) ^ Position.here pos);
         val _ =
           if (exists o Term.exists_subterm) eq_x prems then
             warning ("Induction variable occurs also among premises: " ^
-              quote (Syntax.string_of_term ctxt t) ^ Position.here pos)
+              quote (Syntax.string_of_term goal_ctxt t) ^ Position.here pos)
           else ();
-      in #1 (check_type ctxt (t, pos)) end;
+      in #1 (check_type goal_ctxt (t, pos)) end;
 
-    val argss = map (map (Option.map induct_var)) varss;
+    val argss = (map o map o Option.map) induct_var varss;
     val rule =
       (case opt_rules of
         SOME rules => #2 (Rule_Cases.strict_mutual_rule ctxt rules)