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);