| changeset 6391 | 0da748358eff |
| parent 6114 | 45958e54d72e |
| child 7355 | 4c43090659ca |
--- a/src/FOL/simpdata.ML Wed Mar 17 16:33:00 1999 +0100 +++ b/src/FOL/simpdata.ML Wed Mar 17 16:33:47 1999 +0100 @@ -243,10 +243,10 @@ local val ex_pattern = - read_cterm (sign_of FOL.thy) ("EX x. P(x) & Q(x)", FOLogic.oT) + read_cterm (Theory.sign_of FOL.thy) ("EX x. P(x) & Q(x)", FOLogic.oT) val all_pattern = - read_cterm (sign_of FOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT) + read_cterm (Theory.sign_of FOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT) in val defEX_regroup =