# HG changeset patch
# User paulson
# Date 864204942 -7200
# Node ID 4a3ab8d434519d9eb10c2443bbbb38fe923efa29
# Parent  eca2a3634acde4576a9e61f7549941c449bf5f7c
TFL induction rule is now curried

diff -r eca2a3634acd -r 4a3ab8d43451 src/HOL/ex/Primes.ML
--- a/src/HOL/ex/Primes.ML	Wed May 21 10:55:21 1997 +0200
+++ b/src/HOL/ex/Primes.ML	Wed May 21 10:55:42 1997 +0200
@@ -50,10 +50,7 @@
 val tc = result();
 
 val gcd_eq = tc RS hd gcd.rules;
-val gcd_induct = tc RS gcd.induct 
-                  |> read_instantiate [("P","split Q")]
-                  |> rewrite_rule [split RS eq_reflection]
-                  |> standard;
+val gcd_induct = tc RS gcd.induct;
 
 goal thy "gcd(m,0) = m";
 by (rtac (gcd_eq RS trans) 1);