# HG changeset patch
# User wenzelm
# Date 1154287728 -7200
# Node ID ebe183ff903d5a7a01d4e24a87fe9c9704d23b56
# Parent  5024ba0831a63f9ac85e2191dff161500e976b30
tuned proofs;

diff -r 5024ba0831a6 -r ebe183ff903d src/HOL/Modelcheck/EindhovenSyn.ML
--- 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];
diff -r 5024ba0831a6 -r ebe183ff903d src/HOL/Modelcheck/MuckeSyn.ML
--- 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];