src/ZF/Tools/induct_tacs.ML

--- a/src/ZF/Tools/induct_tacs.ML	Fri Mar 20 11:53:22 2015 +0100
+++ b/src/ZF/Tools/induct_tacs.ML	Fri Mar 20 14:48:04 2015 +0100
@@ -101,7 +101,7 @@
              [] => error "induction is not available for this datatype"
            | major::_ => FOLogic.dest_Trueprop major)
   in
-    eres_inst_tac ctxt [((ixn, Position.none), var)] rule i
+    Rule_Insts.eres_inst_tac ctxt [((ixn, Position.none), var)] rule i
   end
   handle Find_tname msg =>
             if exh then (*try boolean case analysis instead*)