| changeset 5303 | 22029546d109 |
| parent 5069 | 3ea049f7979d |
| child 5553 | ae42b36a50c2 |
--- a/src/HOL/Modelcheck/MCSyn.ML Wed Aug 12 16:16:49 1998 +0200 +++ b/src/HOL/Modelcheck/MCSyn.ML Wed Aug 12 16:20:49 1998 +0200 @@ -26,7 +26,7 @@ local val lhss = [read_cterm (sign_of thy) ("f::'a*'b=>'c", TVar (("'a", 0), []))]; - val rew = mk_meta_eq pair_eta_expand; + val rew = meta_eq pair_eta_expand; fun proc _ _ (Abs _) = Some rew | proc _ _ _ = None;