diff -r f93f7d766895 -r 56610e2ba220 src/HOL/Modelcheck/EindhovenSyn.ML
--- a/src/HOL/Modelcheck/EindhovenSyn.ML	Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/Modelcheck/EindhovenSyn.ML	Tue Aug 06 11:22:05 2002 +0200
@@ -24,16 +24,9 @@
   by (rtac refl 1);
 qed "pair_eta_expand";
 
-local
-  val lhss = [read_cterm (sign_of thy) ("f::'a*'b=>'c", TVar (("'a", 0), []))];
-  val rew = mk_meta_eq pair_eta_expand;
-
-  fun proc _ _ (Abs _) = Some rew
-    | proc _ _ _ = None;
-in
-  val pair_eta_expand_proc = Simplifier.mk_simproc "pair_eta_expand" lhss proc;
-end;
-
+val pair_eta_expand_proc =
+  Simplifier.simproc (Theory.sign_of (the_context ())) "pair_eta_expand" ["f::'a*'b=>'c"]
+  (fn _ => fn _ => fn t => case t of Abs _ => Some (mk_meta_eq pair_eta_expand) | _ => None);
 
 val Eindhoven_ss =
   simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];