# HG changeset patch
# User wenzelm
# Date 1428319734 -7200
# Node ID 5ec4f97dd6d42370089020fbe394dc68191d3e7e
# Parent  bdbc4b761c319ba96112ea7f5c3653d9a02bb30f
proper header;
misc tuning;

diff -r bdbc4b761c31 -r 5ec4f97dd6d4 src/Tools/induction.ML
--- a/src/Tools/induction.ML	Mon Apr 06 12:51:25 2015 +0200
+++ b/src/Tools/induction.ML	Mon Apr 06 13:28:54 2015 +0200
@@ -1,6 +1,14 @@
+(*  Title:      Tools/induction.ML
+    Author:     Tobias Nipkow, TU Muenchen
+
+Alternative proof method "induction" that gives induction hypotheses the
+name "IH".
+*)
+
 signature INDUCTION =
 sig
-  val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
+  val induction_tac: Proof.context -> bool ->
+    (binding option * (term * bool)) option list list ->
     (string * typ) list list -> term option list -> thm list option ->
     thm list -> int -> cases_tactic
 end
@@ -11,13 +19,13 @@
 val ind_hypsN = "IH";
 
 fun preds_of t =
- (case strip_comb t of
+  (case strip_comb t of
     (p as Var _, _) => [p]
   | (p as Free _, _) => [p]
-  | (_, ts) => flat(map preds_of ts))
+  | (_, ts) => maps preds_of ts);
 
 fun name_hyps (arg as ((cases, consumes), th)) =
-  if not(forall (null o #2 o #1) cases) then arg
+  if not (forall (null o #2 o #1) cases) then arg
   else
     let
       val (prems, concl) = Logic.strip_horn (Thm.prop_of th);
@@ -25,18 +33,18 @@
       val ps = preds_of concl;
 
       fun hname_of t =
-        if exists_subterm (member (op =) ps) t
-        then ind_hypsN else Rule_Cases.case_hypsN
+        if exists_subterm (member (op aconv) ps) t
+        then ind_hypsN else Rule_Cases.case_hypsN;
 
-      val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems'
-      val n = Int.min (length hnamess, length cases) 
-      val cases' = map (fn (((cn,_),concls),hns) => ((cn,hns),concls))
-        (take n cases ~~ take n hnamess)
-    in ((cases',consumes),th) end
+      val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems';
+      val n = Int.min (length hnamess, length cases);
+      val cases' =
+        map (fn (((cn, _), concls), hns) => ((cn, hns), concls))
+          (take n cases ~~ take n hnamess);
+    in ((cases', consumes), th) end;
 
-val induction_tac = Induct.gen_induct_tac (K name_hyps)
+val induction_tac = Induct.gen_induct_tac (K name_hyps);
 
-val _ = Theory.setup (Induct.gen_induct_setup @{binding induction} induction_tac)
+val _ = Theory.setup (Induct.gen_induct_setup @{binding induction} induction_tac);
 
 end
-