src/Tools/induction.ML
changeset 59970 e9f73d87d904
parent 59940 087d81f5213e
child 61841 4d3527b94f2a
     1.1 --- a/src/Tools/induction.ML	Wed Apr 08 16:24:22 2015 +0200
     1.2 +++ b/src/Tools/induction.ML	Wed Apr 08 19:39:08 2015 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4            (take n cases ~~ take n hnamess);
     1.5      in ((cases', consumes), th) end;
     1.6  
     1.7 -val induction_tac = Induct.gen_induct_tac (K name_hyps);
     1.8 +val induction_tac = Induct.gen_induct_tac name_hyps;
     1.9  
    1.10  val _ = Theory.local_setup (Induct.gen_induct_setup @{binding induction} induction_tac);
    1.11