src/HOL/Tools/induct_method.ML

 
 signature INDUCT_METHOD =
 sig
   val vars_of: term -> term list
   val concls_of: thm -> term list
+  val rewrite_cterm: thm list -> cterm -> cterm
   val simp_case_tac: bool -> simpset -> int -> tactic
   val setup: (theory -> theory) list
 end;
 
 structure InductMethod: INDUCT_METHOD =

       | prep_var (_, None) = None;
   in
     align "Rule has fewer variables than instantiations given" (vars_of tm) ts
     |> mapfilter prep_var
   end;
+
+fun rewrite_cterm rews =
+  #2 o Thm.dest_comb o #prop o Thm.crep_thm o Simplifier.full_rewrite (HOL_basic_ss addsimps rews);
 
 
 (* simplifying cases rules *)
 
 local

   <x:A> induct ...     - set induction
   ...   induct ... R   - explicit rule
 *)
 
 local
-
-fun rewrite_cterm rews =
-  #2 o Thm.dest_comb o #prop o Thm.crep_thm o Simplifier.full_rewrite (HOL_basic_ss addsimps rews);
 
 fun drop_Trueprop ct =
   let
     fun drop (Abs (x, T, t)) = Abs (x, T, drop t)
       | drop t = HOLogic.dest_Trueprop t;