src/HOL/Product_Type.thy

   |   split_pat tp i _ = None;
   fun metaeq sg lhs rhs = mk_meta_eq (prove_goalw_cterm []
         (cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs))))
         (K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1]));
   val sign = sign_of (the_context ());
-  fun simproc name patstr = Simplifier.mk_simproc name
-                [Thm.read_cterm sign (patstr, HOLogic.termT)];
+  fun simproc name patstr =
+    Simplifier.mk_simproc name [HOLogic.read_cterm sign patstr];
 
   val beta_patstr = "split f z";
   val  eta_patstr = "split f";
   fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t
   |   beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse