--- a/src/HOL/Modelcheck/EindhovenSyn.thy Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Modelcheck/EindhovenSyn.thy Wed Jul 15 23:48:21 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Modelcheck/EindhovenSyn.thy
- ID: $Id$
Author: Olaf Mueller, Jan Philipps, Robert Sandner
Copyright 1997 TU Muenchen
*)
@@ -70,7 +69,7 @@
val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta"));
val pair_eta_expand_proc =
- Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
+ Simplifier.simproc @{theory} "pair_eta_expand" ["f::'a*'b=>'c"]
(fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
val Eindhoven_ss =