diff -r dcd3e7711cac -r ae42b36a50c2 src/HOL/Modelcheck/MCSyn.ML
--- a/src/HOL/Modelcheck/MCSyn.ML	Thu Sep 24 17:16:06 1998 +0200
+++ b/src/HOL/Modelcheck/MCSyn.ML	Thu Sep 24 17:17:14 1998 +0200
@@ -26,7 +26,7 @@
 
 local
   val lhss = [read_cterm (sign_of thy) ("f::'a*'b=>'c", TVar (("'a", 0), []))];
-  val rew = meta_eq pair_eta_expand;
+  val rew = mk_meta_eq pair_eta_expand;
 
   fun proc _ _ (Abs _) = Some rew
     | proc _ _ _ = None;