src/HOL/Product_Type.thy
changeset 12338 de0f4a63baa5
parent 12114 a8e860c86252
child 13462 56610e2ba220
     1.1 --- a/src/HOL/Product_Type.thy	Sat Dec 01 18:51:46 2001 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Sat Dec 01 18:52:32 2001 +0100
     1.3 @@ -342,8 +342,8 @@
     1.4          (cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs))))
     1.5          (K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1]));
     1.6    val sign = sign_of (the_context ());
     1.7 -  fun simproc name patstr = Simplifier.mk_simproc name
     1.8 -                [Thm.read_cterm sign (patstr, HOLogic.termT)];
     1.9 +  fun simproc name patstr =
    1.10 +    Simplifier.mk_simproc name [HOLogic.read_cterm sign patstr];
    1.11  
    1.12    val beta_patstr = "split f z";
    1.13    val  eta_patstr = "split f";