# HG changeset patch
# User wenzelm
# Date 1213200071 -7200
# Node ID bd387c1a05368d934fd2d1b944ede9ca9fffb611
# Parent  a42aef558ce3e5410fab12c4799daf5d489664bc
removed obsolete/unused pred_congs;

diff -r a42aef558ce3 -r bd387c1a0536 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Wed Jun 11 15:41:57 2008 +0200
+++ b/src/FOL/IFOL.thy	Wed Jun 11 18:01:11 2008 +0200
@@ -518,16 +518,6 @@
   apply assumption
   done
 
-(*special cases for free variables P, Q, R, S -- up to 3 arguments*)
-
-ML {*
-bind_thms ("pred_congs",
-  List.concat (map (fn c => 
-               map (fn th => read_instantiate [("P",c)] th)
-                   [@{thm pred1_cong}, @{thm pred2_cong}, @{thm pred3_cong}])
-               (explode"PQRS")))
-*}
-
 (*special case for the equality predicate!*)
 lemma eq_cong: "[| a = a'; b = b' |] ==> a = b <-> a' = b'"
   apply (erule (1) pred2_cong)