--- a/src/HOL/Tools/Datatype/datatype_aux.ML Fri Dec 02 10:31:47 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Fri Dec 02 13:38:24 2011 +0100
@@ -52,7 +52,7 @@
val app_bnds : term -> int -> term
- val indtac : thm -> string list -> int -> tactic
+ val ind_tac : thm -> string list -> int -> tactic
val exh_tac : (string -> thm) -> int -> tactic
exception Datatype
@@ -127,7 +127,7 @@
(* instantiate induction rule *)
-fun indtac indrule indnames = CSUBGOAL (fn (cgoal, i) =>
+fun ind_tac indrule indnames = CSUBGOAL (fn (cgoal, i) =>
let
val cert = cterm_of (Thm.theory_of_cterm cgoal);
val goal = term_of cgoal;