# HG changeset patch
# User wenzelm
# Date 869833908 -7200
# Node ID 0727ebd62b48513250de1a4bef5183115476145f
# Parent  04c6ae944b5e92de58298dfb2d6b35b3e7bef12d
removed split_paired_Ex;
fixed proc args;

diff -r 04c6ae944b5e -r 0727ebd62b48 src/HOL/Modelcheck/MCSyn.ML
--- a/src/HOL/Modelcheck/MCSyn.ML	Fri Jul 25 13:59:15 1997 +0200
+++ b/src/HOL/Modelcheck/MCSyn.ML	Fri Jul 25 14:31:48 1997 +0200
@@ -4,7 +4,7 @@
     Copyright   1997  TU Muenchen
 *)
 
-fun mc_tac i state = 
+fun mc_tac i state =
 let val sign = #sign (rep_thm state)
 in 
 case drop(i-1,prems_of state) of
@@ -18,13 +18,6 @@
 end;
 
 
-goal Prod.thy "(? x. P x) = (? a b. P(a,b))";
-by (Auto_tac());
-by (split_all_tac 1);
-by (Auto_tac());
-qed "split_paired_Ex";
-
-
 goalw thy [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
   by (rtac ext 1);
   by (stac (surjective_pairing RS sym) 1);
@@ -32,15 +25,16 @@
 qed "pair_eta_expand";
 
 local
-  val lhss = [cterm_of (sign_of thy) (read "f::'a*'b=>'c")];
+  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;
+  fun proc _ _ (Abs _) = Some rew
+    | proc _ _ _ = None;
 in
   val pair_eta_expand_proc = Simplifier.mk_simproc "pair_eta_expand" lhss proc;
 end;
 
 
-val MC_ss = (!simpset addsimprocs [pair_eta_expand_proc]) 
-                      addsimps [split_paired_Ex,Let_def];
+val MC_ss =
+  !simpset addsimprocs [pair_eta_expand_proc]
+    addsimps [split_paired_Ex, Let_def];