tuned proofs;

--- a/src/HOL/Modelcheck/EindhovenSyn.ML	Sun Jul 30 05:53:10 2006 +0200
+++ b/src/HOL/Modelcheck/EindhovenSyn.ML	Sun Jul 30 21:28:48 2006 +0200
@@ -10,15 +10,11 @@
     val assertion = mc_eindhoven_oracle thy (Logic.strip_imp_concl goal);
   in cut_facts_tac [assertion] i THEN atac i end) i state;
 
-Goalw [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
-  by (rtac ext 1);
-  by (stac (surjective_pairing RS sym) 1);
-  by (rtac refl 1);
-qed "pair_eta_expand";
+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"]
-  (fn _ => fn _ => fn t => case t of Abs _ => SOME (mk_meta_eq pair_eta_expand) | _ => NONE);
+  (fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
 
 val Eindhoven_ss =
   simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];

--- a/src/HOL/Modelcheck/MuckeSyn.ML	Sun Jul 30 05:53:10 2006 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.ML	Sun Jul 30 21:28:48 2006 +0200
@@ -141,20 +141,14 @@
 
 end;
 
+
 (* first simplification, then model checking *)
 
-goalw (theory "Product_Type") [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
-  by (rtac ext 1);
-  by (stac (surjective_pairing RS sym) 1);
-  by (rtac refl 1);
-qed "pair_eta_expand";
+val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta"));
 
 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);
+  Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
+  (fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
 
 val Mucke_ss = simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];