| changeset 15001 | fb2141a9f8c0 |
| parent 14981 | e73f8140af78 |
| child 15531 | 08c8dad8e399 |
--- a/src/Pure/Proof/proofchecker.ML Wed Jun 23 09:09:18 2004 +0200 +++ b/src/Pure/Proof/proofchecker.ML Wed Jun 23 14:44:22 2004 +0200 @@ -28,7 +28,7 @@ end; val beta_eta_convert = - MetaSimplifier.fconv_rule MetaSimplifier.beta_eta_conversion; + Drule.fconv_rule Drule.beta_eta_conversion; fun thm_of_proof thy prf = let