# HG changeset patch
# User oheimb
# Date 903960160 -7200
# Node ID 1c6f723510752659070fa2a68c4587a3da788f91
# Parent  9daf0136db6a05490473d2b1731ae5ccc956faf2
debugged split_eta_proc

diff -r 9daf0136db6a -r 1c6f72351075 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Fri Aug 21 17:49:21 1998 +0200
+++ b/src/HOL/Prod.ML	Mon Aug 24 14:02:40 1998 +0200
@@ -165,7 +165,7 @@
 			then Some f else None
   |   split_pat k (Const ("split", _) $ Abs (_, _, t)) = split_pat (k+1) t
   |   split_pat k _ = None;
-  fun proc _ _	(s as
+  fun proc sg _	(s as
 	(Const ("split", _) $ Abs (_, _, 
 	(Const ("split", _) $ Abs (_, _, t))))) = (case split_pat 2 t of
 	  Some f => (let val fvar = Free ("f", fastype_of f);
@@ -173,7 +173,7 @@
 			 and atom     (Abs (x, T, t)) = Abs (x, T,atom_fun t)
 			   | atom     (t $ u)         = atom_fun t $ atom_fun u
 			   | atom     x               = x;
-			 val ct   = cterm_of (sign_of thy) (HOLogic.mk_Trueprop
+			 val ct   = cterm_of sg (HOLogic.mk_Trueprop
 				   (HOLogic.mk_eq (atom_fun s,fvar)));
 			 val ss   = HOL_basic_ss addsimps [cond_split_eta];
          in Some (meta_eq (prove_goalw_cterm [] ct (K [simp_tac ss 1]))) end)