1.1 --- a/src/HOL/Transitive_Closure.thy	Fri Feb 20 14:22:51 2004 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Sat Feb 21 08:43:08 2004 +0100
     1.3 @@ -70,11 +70,10 @@
     1.4    thus ?thesis by rules
     1.5  qed
     1.6  
     1.7 -ML_setup {*
     1.8 -  bind_thm ("rtrancl_induct2", split_rule
     1.9 -    (read_instantiate [("a","(ax,ay)"), ("b","(bx,by)")] (thm "rtrancl_induct")));
    1.10 -*}
    1.11 -
    1.12 +lemmas rtrancl_induct2 =
    1.13 +  rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
    1.14 +                 consumes 1, case_names refl step]
    1.15 + 
    1.16  lemma trans_rtrancl: "trans(r^*)"
    1.17    -- {* transitivity of transitive closure!! -- by induction *}
    1.18  proof (rule transI)
    1.19 @@ -165,7 +164,7 @@
    1.20  lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"
    1.21    by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI)
    1.22  
    1.23 -theorem converse_rtrancl_induct:
    1.24 +theorem converse_rtrancl_induct[consumes 1]:
    1.25    assumes major: "(a, b) : r^*"
    1.26      and cases: "P b" "!!y z. [| (y, z) : r; (z, b) : r^*; P z |] ==> P y"
    1.27    shows "P a"
    1.28 @@ -175,10 +174,9 @@
    1.29      by induct (rules intro: cases dest!: converseD rtrancl_converseD)+
    1.30  qed
    1.31  
    1.32 -ML_setup {*
    1.33 -  bind_thm ("converse_rtrancl_induct2", split_rule
    1.34 -    (read_instantiate [("a","(ax,ay)"),("b","(bx,by)")] (thm "converse_rtrancl_induct")));
    1.35 -*}
    1.36 +lemmas converse_rtrancl_induct2 =
    1.37 +  converse_rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
    1.38 +                 consumes 1, case_names refl step]
    1.39  
    1.40  lemma converse_rtranclE:
    1.41    "[| (x,z):r^*;