# HG changeset patch
# User wenzelm
# Date 1278961938 -7200
# Node ID 7e91b3f98c468e7f2a11f0d42ff3aa0a09bef8a8
# Parent  982b0668dcbd731baa3fe126882b8bd1691c16a8
eliminated OldGoals.strip_context;

diff -r 982b0668dcbd -r 7e91b3f98c46 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Mon Jul 12 20:35:10 2010 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Mon Jul 12 21:12:18 2010 +0200
@@ -68,13 +68,16 @@
 (*Given a variable, find the inductive set associated it in the assumptions*)
 exception Find_tname of string
 
-fun find_tname var Bi =
+fun find_tname ctxt var As =
   let fun mk_pair (Const(@{const_name mem},_) $ Free (v,_) $ A) =
              (v, #1 (dest_Const (head_of A)))
         | mk_pair _ = raise Match
-      val pairs = map_filter (try (mk_pair o FOLogic.dest_Trueprop))
-          (#2 (OldGoals.strip_context Bi))
-  in case AList.lookup (op =) pairs var of
+      val pairs = map_filter (try (mk_pair o FOLogic.dest_Trueprop)) As
+      val x =
+        (case try (dest_Free o Syntax.read_term ctxt) var of
+          SOME (x, _) => x
+        | _ => raise Find_tname ("Bad variable " ^ quote var))
+  in case AList.lookup (op =) pairs x of
        NONE => raise Find_tname ("Cannot determine datatype of " ^ quote var)
      | SOME t => t
   end;
@@ -89,8 +92,8 @@
 fun exhaust_induct_tac exh ctxt var i state =
   let
     val thy = ProofContext.theory_of ctxt
-    val (_, _, Bi, _) = Thm.dest_state (state, i)
-    val tn = find_tname var Bi
+    val ({context = ctxt', asms, ...}, _) = Subgoal.focus ctxt i state
+    val tn = find_tname ctxt' var (map term_of asms)
     val rule =
         if exh then #exhaustion (datatype_info thy tn)
                else #induct  (datatype_info thy tn)