src/HOL/Product_Type.thy

   Simplification procedure for @{thm [source] unit_eq}.  Cannot use
   this rule directly --- it loops!
 *}
 
 ML_setup {*
-  local
-    val unit_pat = Thm.cterm_of (Theory.sign_of (the_context ())) (Free ("x", HOLogic.unitT));
-    val unit_meta_eq = standard (mk_meta_eq (thm "unit_eq"));
-    fun proc _ _ t =
-      if HOLogic.is_unit t then None
-      else Some unit_meta_eq
-  in val unit_eq_proc = Simplifier.mk_simproc "unit_eq" [unit_pat] proc end;
+  val unit_eq_proc =
+    let val unit_meta_eq = mk_meta_eq (thm "unit_eq") in
+      Simplifier.simproc (Theory.sign_of (the_context ())) "unit_eq" ["x::unit"]
+      (fn _ => fn _ => fn t => if HOLogic.is_unit t then None else Some unit_meta_eq)
+    end;
 
   Addsimprocs [unit_eq_proc];
 *}
 
 lemma unit_all_eq1: "(!!x::unit. PROP P x) == PROP P ()"

   |   split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t
   |   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 [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
                         (beta_term_pat k i t andalso beta_term_pat k i u)
   |   beta_term_pat k i t = no_args k i t;
   fun  eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg

         (case split_pat eta_term_pat 1 t of
           Some (_,ft) => Some (metaeq sg s (let val (f $ arg) = ft in f end))
         | None => None)
   |   eta_proc _ _ _ = None;
 in
-  val split_beta_proc = simproc "split_beta" beta_patstr beta_proc;
-  val split_eta_proc  = simproc "split_eta"   eta_patstr  eta_proc;
+  val split_beta_proc = Simplifier.simproc (Theory.sign_of (the_context ()))
+    "split_beta" ["split f z"] beta_proc;
+  val split_eta_proc = Simplifier.simproc (Theory.sign_of (the_context ()))
+    "split_eta" ["split f"] eta_proc;
 end;
 
 Addsimprocs [split_beta_proc, split_eta_proc];
 *}