changeset 26480 | 544cef16045b |
parent 26322 | eaf634e975fa |
child 26956 | 1309a6a0a29f |
--- a/src/FOLP/IFOLP.thy Sat Mar 29 19:13:58 2008 +0100 +++ b/src/FOLP/IFOLP.thy Sat Mar 29 19:14:00 2008 +0100 @@ -502,7 +502,7 @@ (*special cases for free variables P, Q, R, S -- up to 3 arguments*) -ML_setup {* +ML {* bind_thms ("pred_congs", flat (map (fn c => map (fn th => read_instantiate [("P",c)] th)