--- 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];