src/ZF/Tools/induct_tacs.ML

--- a/src/ZF/Tools/induct_tacs.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Sat May 15 21:50:05 2010 +0200
@@ -89,7 +89,7 @@
 fun exhaust_induct_tac exh ctxt var i state =
   let
     val thy = ProofContext.theory_of ctxt
-    val (_, _, Bi, _) = dest_state (state, i)
+    val (_, _, Bi, _) = Thm.dest_state (state, i)
     val tn = find_tname var Bi
     val rule =
         if exh then #exhaustion (datatype_info thy tn)