1.1 --- a/src/HOL/Prod.ML	Fri Aug 21 17:49:21 1998 +0200
     1.2 +++ b/src/HOL/Prod.ML	Mon Aug 24 14:02:40 1998 +0200
     1.3 @@ -165,7 +165,7 @@
     1.4  			then Some f else None
     1.5    |   split_pat k (Const ("split", _) $ Abs (_, _, t)) = split_pat (k+1) t
     1.6    |   split_pat k _ = None;
     1.7 -  fun proc _ _	(s as
     1.8 +  fun proc sg _	(s as
     1.9  	(Const ("split", _) $ Abs (_, _, 
    1.10  	(Const ("split", _) $ Abs (_, _, t))))) = (case split_pat 2 t of
    1.11  	  Some f => (let val fvar = Free ("f", fastype_of f);
    1.12 @@ -173,7 +173,7 @@
    1.13  			 and atom     (Abs (x, T, t)) = Abs (x, T,atom_fun t)
    1.14  			   | atom     (t $ u)         = atom_fun t $ atom_fun u
    1.15  			   | atom     x               = x;
    1.16 -			 val ct   = cterm_of (sign_of thy) (HOLogic.mk_Trueprop
    1.17 +			 val ct   = cterm_of sg (HOLogic.mk_Trueprop
    1.18  				   (HOLogic.mk_eq (atom_fun s,fvar)));
    1.19  			 val ss   = HOL_basic_ss addsimps [cond_split_eta];
    1.20           in Some (meta_eq (prove_goalw_cterm [] ct (K [simp_tac ss 1]))) end)