src/HOL/Tools/function_package/induction_scheme.ML

 (*  Title:      HOL/Tools/function_package/induction_scheme.ML
-    ID:         $Id$
     Author:     Alexander Krauss, TU Muenchen
 
 A method to prove induction schemes.
 *)
 
 signature INDUCTION_SCHEME =
 sig
   val mk_ind_tac : (int -> tactic) -> (int -> tactic) -> (int -> tactic)
-                   -> Proof.context -> thm list -> tactic  
+                   -> Proof.context -> thm list -> tactic
+  val induct_scheme_tac : Proof.context -> thm list -> tactic
   val setup : theory -> theory
 end
 
 
 structure InductionScheme : INDUCTION_SCHEME =

     THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches))))
     THEN (EVERY (map (TRY o comp_tac) ((i + nbranches - 1) downto i)))
   end))
 
 
+fun induct_scheme_tac ctxt =
+  mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt;
+
 val setup = Method.add_methods
-  [("induct_scheme", Method.ctxt_args (Method.RAW_METHOD o (fn ctxt => mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt)),
+  [("induct_scheme", Method.ctxt_args (Method.RAW_METHOD o induct_scheme_tac),
     "proves an induction principle")]
 
 end