# HG changeset patch
# User wenzelm
# Date 1460139320 -7200
# Node ID 13252110a6fe1c2c0dfb75779a878684d964f048
# Parent  745d31e63c21b80278a8a4315bb23ee18c78b8f4
eliminated unused simproc identifier;

diff -r 745d31e63c21 -r 13252110a6fe src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy	Fri Apr 08 20:15:20 2016 +0200
@@ -794,8 +794,7 @@
 
   @{rail \<open>
     @@{command simproc_setup} @{syntax name} '(' (@{syntax term} + '|') ')' '='
-      @{syntax text} \<newline> (@'identifier' (@{syntax nameref}+))?
-    ;
+      @{syntax text};
 
     @@{attribute simproc} (('add' ':')? | 'del' ':') (@{syntax name}+)
   \<close>}
@@ -810,12 +809,10 @@
   NONE} to indicate failure. The @{ML_type Proof.context} argument holds the
   full context of the current Simplifier invocation. The @{ML_type morphism}
   informs about the difference of the original compilation context wrt.\ the
-  one of the actual application later on. The optional @{keyword "identifier"}
-  specifies theorems that represent the logical content of the abstract theory
-  of this simproc.
+  one of the actual application later on.
 
-  Morphisms and identifiers are only relevant for simprocs that are defined
-  within a local target context, e.g.\ in a locale.
+  Morphisms are only relevant for simprocs that are defined within a local
+  target context, e.g.\ in a locale.
 
   \<^descr> \<open>simproc add: name\<close> and \<open>simproc del: name\<close> add or delete named simprocs
   to the current Simplifier context. The default is to add a simproc. Note
diff -r 745d31e63c21 -r 13252110a6fe src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Decision_Procs/langford.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -171,7 +171,7 @@
 
 val reduce_ex_simproc =
   Simplifier.make_simproc @{context} "reduce_ex_simproc"
-    {lhss = [@{term "\<exists>x. P x"}], proc = K proc, identifier = []};
+    {lhss = [@{term "\<exists>x. P x"}], proc = K proc};
 
 end;
 
diff -r 745d31e63c21 -r 13252110a6fe src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/HOL.thy	Fri Apr 08 20:15:20 2016 +0200
@@ -1444,8 +1444,7 @@
           (case Thm.term_of ct of
             _ $ (P as _ $ @{const induct_false}) $ (_ $ Q $ _) =>
               if P <> Q then SOME Drule.swap_prems_eq else NONE
-          | _ => NONE),
-         identifier = []},
+          | _ => NONE)},
        Simplifier.make_simproc @{context} "induct_equal_conj_curry"
         {lhss = [@{term "induct_conj P Q \<Longrightarrow> PROP R"}],
          proc = fn _ => fn _ => fn ct =>
@@ -1459,8 +1458,7 @@
                   | is_conj @{const induct_false} = true
                   | is_conj _ = false
               in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
-            | _ => NONE),
-          identifier = []}]
+            | _ => NONE)}]
     |> Simplifier.set_mksimps (fn ctxt =>
         Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
         map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback}))))
@@ -1759,8 +1757,7 @@
          proc = fn _ => fn _ => fn ct =>
           (case Thm.term_of ct of
             Const (_, Type (@{type_name fun}, [Type _, _])) => SOME @{thm eq_equal}
-          | _ => NONE),
-         identifier = []}])
+          | _ => NONE)}])
 \<close>
 
 
diff -r 745d31e63c21 -r 13252110a6fe src/HOL/HOLCF/Tools/cont_proc.ML
--- a/src/HOL/HOLCF/Tools/cont_proc.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -127,7 +127,7 @@
 in
   val cont_proc =
     Simplifier.make_simproc @{context} "cont_proc"
-     {lhss = [@{term "cont f"}], proc = K solve_cont, identifier = []}
+     {lhss = [@{term "cont f"}], proc = K solve_cont}
 end
 
 val setup = map_theory_simpset (fn ctxt => ctxt addsimprocs [cont_proc])
diff -r 745d31e63c21 -r 13252110a6fe src/HOL/Library/Old_SMT/old_smt_real.ML
--- a/src/HOL/Library/Old_SMT/old_smt_real.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Library/Old_SMT/old_smt_real.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -117,7 +117,7 @@
 val real_linarith_proc =
   Simplifier.make_simproc @{context} "fast_real_arith"
    {lhss = [@{term "(m::real) < n"}, @{term "(m::real) \<le> n"}, @{term "(m::real) = n"}],
-    proc = K Lin_Arith.simproc, identifier = []}
+    proc = K Lin_Arith.simproc}
 
 
 (* setup *)
diff -r 745d31e63c21 -r 13252110a6fe src/HOL/Library/Old_SMT/old_z3_proof_tools.ML
--- a/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -345,13 +345,13 @@
       addsimprocs [
         Simplifier.make_simproc @{context} "fast_int_arith"
          {lhss = [@{term "(m::int) < n"}, @{term "(m::int) \<le> n"}, @{term "(m::int) = n"}],
-          proc = K Lin_Arith.simproc, identifier = []},
+          proc = K Lin_Arith.simproc},
         Simplifier.make_simproc @{context} "antisym_le"
          {lhss = [@{term "(x::'a::order) \<le> y"}],
-          proc = K prove_antisym_le, identifier = []},
+          proc = K prove_antisym_le},
         Simplifier.make_simproc @{context} "antisym_less"
          {lhss = [@{term "\<not> (x::'a::linorder) < y"}],
-          proc = K prove_antisym_less, identifier = []}])
+          proc = K prove_antisym_less}])
 
   structure Simpset = Generic_Data
   (
diff -r 745d31e63c21 -r 13252110a6fe src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -122,7 +122,7 @@
 
 val perm_simproc =
   Simplifier.make_simproc @{context} "perm_simp"
-   {lhss = [@{term "pi1 \<bullet> (pi2 \<bullet> x)"}], proc = K perm_simproc', identifier = []};
+   {lhss = [@{term "pi1 \<bullet> (pi2 \<bullet> x)"}], proc = K perm_simproc'};
 
 fun projections ctxt rule =
   Project_Rule.projections ctxt rule
diff -r 745d31e63c21 -r 13252110a6fe src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -47,8 +47,7 @@
         Const (@{const_name Nominal.perm}, _) $ _ $ t =>
           if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
           then SOME perm_bool else NONE
-      | _ => NONE),
-    identifier = []};
+      | _ => NONE)};
 
 fun transp ([] :: _) = []
   | transp xs = map hd xs :: transp (map tl xs);
diff -r 745d31e63c21 -r 13252110a6fe src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -51,8 +51,7 @@
         Const (@{const_name Nominal.perm}, _) $ _ $ t =>
           if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
           then SOME perm_bool else NONE
-       | _ => NONE),
-    identifier = []};
+       | _ => NONE)};
 
 fun transp ([] :: _) = []
   | transp xs = map hd xs :: transp (map tl xs);
diff -r 745d31e63c21 -r 13252110a6fe src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -114,7 +114,7 @@
 
 val perm_simproc_app =
   Simplifier.make_simproc @{context} "perm_simproc_app"
-   {lhss = [@{term "Nominal.perm pi x"}], proc = K perm_simproc_app', identifier = []}
+   {lhss = [@{term "Nominal.perm pi x"}], proc = K perm_simproc_app'}
 
 (* a simproc that deals with permutation instances in front of functions  *)
 fun perm_simproc_fun' ctxt ct =
@@ -136,7 +136,7 @@
 
 val perm_simproc_fun =
   Simplifier.make_simproc @{context} "perm_simproc_fun"
-   {lhss = [@{term "Nominal.perm pi x"}], proc = K perm_simproc_fun', identifier = []}
+   {lhss = [@{term "Nominal.perm pi x"}], proc = K perm_simproc_fun'}
 
 (* function for simplyfying permutations          *)
 (* stac contains the simplifiation tactic that is *)
@@ -219,7 +219,7 @@
 val perm_compose_simproc =
   Simplifier.make_simproc @{context} "perm_compose"
    {lhss = [@{term "Nominal.perm pi1 (Nominal.perm pi2 t)"}],
-    proc = K perm_compose_simproc', identifier = []}
+    proc = K perm_compose_simproc'}
 
 fun perm_compose_tac ctxt i =
   ("analysing permutation compositions on the lhs",
diff -r 745d31e63c21 -r 13252110a6fe src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Product_Type.thy	Fri Apr 08 20:15:20 2016 +0200
@@ -1327,8 +1327,7 @@
   Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs
     [Simplifier.make_simproc @{context} "set comprehension"
       {lhss = [@{term "Collect P"}],
-       proc = K Set_Comprehension_Pointfree.code_simproc,
-       identifier = []}])
+       proc = K Set_Comprehension_Pointfree.code_simproc}])
 \<close>
 
 
diff -r 745d31e63c21 -r 13252110a6fe src/HOL/Statespace/distinct_tree_prover.ML
--- a/src/HOL/Statespace/distinct_tree_prover.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -360,8 +360,7 @@
         Const (@{const_name HOL.eq}, _) $ x $ y =>
           Option.map (fn neq => @{thm neq_to_eq_False} OF [neq])
             (get_fst_success (neq_x_y ctxt x y) names)
-      | _ => NONE),
-    identifier = []};
+      | _ => NONE)};
 
 end;
 
diff -r 745d31e63c21 -r 13252110a6fe src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Statespace/state_fun.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -72,8 +72,7 @@
                 else SOME (conj_cong OF [P_P', Q_Q'])
               end
            end
-      | _ => NONE),
-    identifier = []};
+      | _ => NONE)};
 
 fun string_eq_simp_tac ctxt =
   simp_tac (put_simpset HOL_basic_ss ctxt
@@ -154,8 +153,7 @@
           else SOME thm
         end
         handle Option.Option => NONE)
-      | _ => NONE),
-  identifier = []};
+      | _ => NONE)};
 
 
 local
@@ -260,8 +258,7 @@
                 in SOME (Thm.transitive eq1 eq2) end
             | _ => NONE)
           end
-      | _ => NONE),
-  identifier = []};
+      | _ => NONE)};
 
 end;
 
@@ -326,8 +323,7 @@
               val thm' = if swap then swap_ex_eq OF [thm] else thm
             in SOME thm' end handle TERM _ => NONE)
         | _ => NONE)
-      end handle Option.Option => NONE,
-  identifier = []};
+      end handle Option.Option => NONE};
 
 end;
 
diff -r 745d31e63c21 -r 13252110a6fe src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Statespace/state_space.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -218,8 +218,7 @@
         Const (@{const_name HOL.eq},_) $ (x as Free _) $ (y as Free _) =>
           Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq])
             (neq_x_y ctxt x y)
-      | _ => NONE),
-    identifier = []};
+      | _ => NONE)};
 
 fun interprete_parent name dist_thm_name parent_expr thy =
   let
diff -r 745d31e63c21 -r 13252110a6fe src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -150,8 +150,7 @@
 val regularize_simproc =
   Simplifier.make_simproc @{context} "regularize"
     {lhss = [@{term "Ball (Respects (R1 ===> R2)) P"}, @{term "Bex (Respects (R1 ===> R2)) P"}],
-     proc = K ball_bex_range_simproc,
-     identifier = []};
+     proc = K ball_bex_range_simproc};
 
 fun regularize_tac ctxt =
   let
diff -r 745d31e63c21 -r 13252110a6fe src/HOL/Tools/SMT/smt_real.ML
--- a/src/HOL/Tools/SMT/smt_real.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Tools/SMT/smt_real.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -101,7 +101,7 @@
 val real_linarith_proc =
   Simplifier.make_simproc @{context} "fast_real_arith"
    {lhss = [@{term "(m::real) < n"}, @{term "(m::real) \<le> n"}, @{term "(m::real) = n"}],
-    proc = K Lin_Arith.simproc, identifier = []}
+    proc = K Lin_Arith.simproc}
 
 
 (* setup *)
diff -r 745d31e63c21 -r 13252110a6fe src/HOL/Tools/SMT/z3_replay_util.ML
--- a/src/HOL/Tools/SMT/z3_replay_util.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Tools/SMT/z3_replay_util.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -126,13 +126,13 @@
       addsimprocs [@{simproc numeral_divmod},
         Simplifier.make_simproc @{context} "fast_int_arith"
          {lhss = [@{term "(m::int) < n"}, @{term "(m::int) \<le> n"}, @{term "(m::int) = n"}],
-          proc = K Lin_Arith.simproc, identifier = []},
+          proc = K Lin_Arith.simproc},
         Simplifier.make_simproc @{context} "antisym_le"
          {lhss = [@{term "(x::'a::order) \<le> y"}],
-          proc = K prove_antisym_le, identifier = []},
+          proc = K prove_antisym_le},
         Simplifier.make_simproc @{context} "antisym_less"
          {lhss = [@{term "\<not> (x::'a::linorder) < y"}],
-          proc = K prove_antisym_less, identifier = []}])
+          proc = K prove_antisym_less}])
 
   structure Simpset = Generic_Data
   (
diff -r 745d31e63c21 -r 13252110a6fe src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Tools/groebner.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -787,7 +787,7 @@
   in
     Simplifier.cert_simproc (Thm.theory_of_thm idl_sub) "poly_eq_simproc"
      {lhss = [Thm.term_of (Thm.lhs_of idl_sub)],
-      proc = fn _ => fn _ => proc, identifier = []}
+      proc = fn _ => fn _ => proc}
   end;
 
 val poly_eq_ss =
diff -r 745d31e63c21 -r 13252110a6fe src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -98,8 +98,7 @@
               end
             else NONE
         | _ => NONE)
-      end,
-    identifier = []};
+      end};
 
 (* only eta contract terms occurring as arguments of functions satisfying p *)
 fun eta_contract p =
@@ -319,8 +318,7 @@
       {lhss = [anyt],
        proc = fn _ => fn ctxt => fn ct =>
         lookup_rule (Proof_Context.theory_of ctxt)
-          (Thm.prop_of #> Logic.dest_equals) rules' (Thm.term_of ct),
-       identifier = []}
+          (Thm.prop_of #> Logic.dest_equals) rules' (Thm.term_of ct)}
   end;
 
 fun to_pred_proc thy rules t =
diff -r 745d31e63c21 -r 13252110a6fe src/HOL/Tools/int_arith.ML
--- a/src/HOL/Tools/int_arith.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Tools/int_arith.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -29,8 +29,7 @@
       let val T = Thm.ctyp_of_cterm ct in
         if Thm.typ_of T = @{typ int} then NONE
         else SOME (Thm.instantiate' [SOME T] [] zeroth)
-      end,
-     identifier = []};
+      end};
 
 val oneth = Thm.symmetric (mk_meta_eq @{thm of_int_1});
 
@@ -41,8 +40,7 @@
       let val T = Thm.ctyp_of_cterm ct in
         if Thm.typ_of T = @{typ int} then NONE
         else SOME (Thm.instantiate' [SOME T] [] oneth)
-      end,
-    identifier = []};
+      end};
 
 fun check (Const (@{const_name Groups.one}, @{typ int})) = false
   | check (Const (@{const_name Groups.one}, _)) = true
@@ -71,8 +69,7 @@
     proc = fn _ => fn ctxt => fn ct =>
       if check (Thm.term_of ct)
       then SOME (Simplifier.rewrite (put_simpset conv_ss ctxt) ct)
-      else NONE,
-    identifier = []};
+      else NONE};
 
 
 fun number_of ctxt T n =
diff -r 745d31e63c21 -r 13252110a6fe src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -451,16 +451,14 @@
       @{term "((numeral v)::'a::field) / (- numeral w)"},
       @{term "((- numeral v)::'a::field) / (numeral w)"},
       @{term "((- numeral v)::'a::field) / (- numeral w)"}],
-    proc = K DivideCancelNumeralFactor.proc,
-    identifier = []}
+    proc = K DivideCancelNumeralFactor.proc}
 
 val field_cancel_numeral_factors =
   [Simplifier.make_simproc @{context} "field_eq_cancel_numeral_factor"
     {lhss =
        [@{term "(l::'a::field) * m = n"},
         @{term "(l::'a::field) = m * n"}],
-      proc = K EqCancelNumeralFactor.proc,
-      identifier = []},
+      proc = K EqCancelNumeralFactor.proc},
    field_divide_cancel_numeral_factor]
 
 
@@ -693,12 +691,12 @@
 val add_frac_frac_simproc =
   Simplifier.make_simproc @{context} "add_frac_frac_simproc"
    {lhss = [@{term "(x::'a::field) / y + (w::'a::field) / z"}],
-    proc = K proc, identifier = []}
+    proc = K proc}
 
 val add_frac_num_simproc =
   Simplifier.make_simproc @{context} "add_frac_num_simproc"
    {lhss = [@{term "(x::'a::field) / y + z"}, @{term "z + (x::'a::field) / y"}],
-    proc = K proc2, identifier = []}
+    proc = K proc2}
 
 val ord_frac_simproc =
   Simplifier.make_simproc @{context} "ord_frac_simproc"
@@ -709,7 +707,7 @@
       @{term "c \<le> (a::'a::{field,ord}) / b"},
       @{term "c = (a::'a::{field,ord}) / b"},
       @{term "(a::'a::{field, ord}) / b = c"}],
-    proc = K proc3, identifier = []}
+    proc = K proc3}
 
 val ths =
  [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
diff -r 745d31e63c21 -r 13252110a6fe src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Tools/record.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -1116,8 +1116,7 @@
               end
             else NONE
         | _ => NONE)
-      end,
-    identifier = []};
+      end};
 
 fun get_upd_acc_cong_thm upd acc thy ss =
   let
@@ -1250,8 +1249,7 @@
             (prove_unfold_defs thy noops' [simproc]
               (Logic.list_all (vars, Logic.mk_equals (lhs, rhs))))
         else NONE
-      end,
-    identifier = []};
+      end};
 
 end;
 
@@ -1282,8 +1280,7 @@
               (case get_equalities (Proof_Context.theory_of ctxt) name of
                 NONE => NONE
               | SOME thm => SOME (thm RS @{thm Eq_TrueI})))
-      | _ => NONE),
-    identifier = []};
+      | _ => NONE)};
 
 
 (* split_simproc *)
@@ -1320,8 +1317,7 @@
                   else NONE
                 end)
           else NONE
-      | _ => NONE),
-    identifier = []};
+      | _ => NONE)};
 
 val ex_sel_eq_simproc =
   Simplifier.make_simproc @{context} "ex_sel_eq"
@@ -1362,8 +1358,7 @@
                     addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1))
             end handle TERM _ => NONE)
         | _ => NONE)
-      end,
-    identifier = []};
+      end};
 
 
 (* split_simp_tac *)
diff -r 745d31e63c21 -r 13252110a6fe src/HOL/Word/WordBitwise.thy
--- a/src/HOL/Word/WordBitwise.thy	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Word/WordBitwise.thy	Fri Apr 08 20:15:20 2016 +0200
@@ -525,7 +525,7 @@
 
 val expand_upt_simproc =
   Simplifier.make_simproc @{context} "expand_upt"
-   {lhss = [@{term "upt x y"}], proc = K upt_conv, identifier = []};
+   {lhss = [@{term "upt x y"}], proc = K upt_conv};
 
 fun word_len_simproc_fn ctxt ct =
   case Thm.term_of ct of
@@ -541,7 +541,7 @@
 
 val word_len_simproc =
   Simplifier.make_simproc @{context} "word_len"
-   {lhss = [@{term "len_of x"}], proc = K word_len_simproc_fn, identifier = []};
+   {lhss = [@{term "len_of x"}], proc = K word_len_simproc_fn};
 
 (* convert 5 or nat 5 to Suc 4 when n_sucs = 1, Suc (Suc 4) when n_sucs = 2,
    or just 5 (discarding nat) when n_sucs = 0 *)
@@ -568,7 +568,7 @@
 fun nat_get_Suc_simproc n_sucs ts =
   Simplifier.make_simproc @{context} "nat_get_Suc"
    {lhss = map (fn t => t $ @{term "n :: nat"}) ts,
-    proc = K (nat_get_Suc_simproc_fn n_sucs), identifier = []};
+    proc = K (nat_get_Suc_simproc_fn n_sucs)};
 
 val no_split_ss =
   simpset_of (put_simpset HOL_ss @{context}
diff -r 745d31e63c21 -r 13252110a6fe src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -18,7 +18,7 @@
   val oracle: bstring * Position.range -> Input.source -> theory -> theory
   val declaration: {syntax: bool, pervasive: bool} -> Input.source -> local_theory -> local_theory
   val simproc_setup: string * Position.T -> string list -> Input.source ->
-    string list -> local_theory -> local_theory
+    local_theory -> local_theory
   val qed: Method.text_range option -> Toplevel.transition -> Toplevel.transition
   val terminal_proof: Method.text_range * Method.text_range option ->
     Toplevel.transition -> Toplevel.transition
@@ -151,14 +151,13 @@
 
 (* simprocs *)
 
-fun simproc_setup name lhss source identifier =
+fun simproc_setup name lhss source =
   ML_Lex.read_source false source
   |> ML_Context.expression (Input.range_of source) "proc"
     "Morphism.morphism -> Proof.context -> cterm -> thm option"
     ("Context.map_proof (Simplifier.define_simproc_cmd " ^
       ML_Syntax.atomic (ML_Syntax.make_binding name) ^
-      "{lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
-      \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})")
+      "{lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc})")
   |> Context.proof_map;
 
 
diff -r 745d31e63c21 -r 13252110a6fe src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/Pure/ML/ml_context.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -6,9 +6,6 @@
 
 signature ML_CONTEXT =
 sig
-  val thm: xstring -> thm
-  val thms: xstring -> thm list
-  val exec: (unit -> unit) -> Context.generic -> Context.generic
   val check_antiquotation: Proof.context -> xstring * Position.T -> string
   val struct_name: Proof.context -> string
   val variant: string -> Proof.context -> string * Proof.context
@@ -23,6 +20,7 @@
   val eval_in: Proof.context option -> ML_Compiler.flags -> Position.T ->
     ML_Lex.token Antiquote.antiquote list -> unit
   val eval_source_in: Proof.context option -> ML_Compiler.flags -> Input.source -> unit
+  val exec: (unit -> unit) -> Context.generic -> Context.generic
   val expression: Position.range -> string -> string -> string ->
     ML_Lex.token Antiquote.antiquote list -> Context.generic -> Context.generic
 end
@@ -30,19 +28,6 @@
 structure ML_Context: ML_CONTEXT =
 struct
 
-(** implicit ML context **)
-
-fun thm name = Proof_Context.get_thm (Context.the_local_context ()) name;
-fun thms name = Proof_Context.get_thms (Context.the_local_context ()) name;
-
-fun exec (e: unit -> unit) context =
-  (case Context.setmp_generic_context (SOME context)
-      (fn () => (e (); Context.get_generic_context ())) () of
-    SOME context' => context'
-  | NONE => error "Missing context after execution");
-
-
-
 (** ML antiquotations **)
 
 (* names for generated environment *)
@@ -220,6 +205,12 @@
   Context.setmp_generic_context (Option.map Context.Proof ctxt)
     (fn () => eval_source flags source) ();
 
+fun exec (e: unit -> unit) context =
+  (case Context.setmp_generic_context (SOME context)
+      (fn () => (e (); Context.get_generic_context ())) () of
+    SOME context' => context'
+  | NONE => error "Missing context after execution");
+
 fun expression range name constraint body ants =
   exec (fn () =>
     eval ML_Compiler.flags (#1 range)
diff -r 745d31e63c21 -r 13252110a6fe src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/Pure/Pure.thy	Fri Apr 08 20:15:20 2016 +0200
@@ -9,7 +9,7 @@
     "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>"
     "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
     "\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
-    "defines" "rewrites" "fixes" "for" "identifier" "if" "in" "includes" "infix"
+    "defines" "rewrites" "fixes" "for" "if" "in" "includes" "infix"
     "infixl" "infixr" "is" "notes" "obtains" "open" "output"
     "overloaded" "pervasive" "premises" "private" "qualified" "rewrites"
     "shows" "structure" "unchecked" "where" "when" "|"
@@ -210,8 +210,7 @@
   Outer_Syntax.local_theory @{command_keyword simproc_setup} "define simproc in ML"
     (Parse.position Parse.name --
       (@{keyword "("} |-- Parse.enum1 "|" Parse.term --| @{keyword ")"} --| @{keyword "="}) --
-      Parse.ML_source -- Scan.optional (@{keyword "identifier"} |-- Scan.repeat1 Parse.xname) []
-    >> (fn (((a, b), c), d) => Isar_Cmd.simproc_setup a b c d));
+      Parse.ML_source >> (fn ((a, b), c) => Isar_Cmd.simproc_setup a b c));
 
 in end\<close>
 
diff -r 745d31e63c21 -r 13252110a6fe src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/Pure/raw_simplifier.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -36,8 +36,7 @@
   type simproc
   val eq_simproc: simproc * simproc -> bool
   val cert_simproc: theory -> string ->
-    {lhss: term list, proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list}
-    -> simproc
+    {lhss: term list, proc: morphism -> Proof.context -> cterm -> thm option} -> simproc
   val transform_simproc: morphism -> simproc -> simproc
   val simpset_of: Proof.context -> simpset
   val put_simpset: simpset -> Proof.context -> Proof.context
@@ -220,12 +219,9 @@
    {name: string,
     lhs: term,
     proc: Proof.context -> cterm -> thm option,
-    id: stamp * thm list};
+    stamp: stamp};
 
-fun eq_procid ((s1: stamp, ths1: thm list), (s2, ths2)) =
-  s1 = s2 andalso eq_list Thm.eq_thm (ths1, ths2);
-
-fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = eq_procid (id1, id2);
+fun eq_proc (Proc {stamp = stamp1, ...}, Proc {stamp = stamp2, ...}) = stamp1 = stamp2;
 
 
 (* solvers *)
@@ -298,8 +294,8 @@
  {simps = Net.entries rules
     |> map (fn {name, thm, ...} => (name, thm)),
   procs = Net.entries procs
-    |> map (fn Proc {name, lhs, id, ...} => ((name, lhs), id))
-    |> partition_eq (eq_snd eq_procid)
+    |> map (fn Proc {name, lhs, stamp, ...} => ((name, lhs), stamp))
+    |> partition_eq (eq_snd op =)
     |> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)),
   congs = #1 congs,
   weak_congs = #2 congs,
@@ -667,20 +663,19 @@
     {name: string,
      lhss: term list,
      proc: morphism -> Proof.context -> cterm -> thm option,
-     id: stamp * thm list};
+     stamp: stamp};
 
-fun eq_simproc (Simproc {id = id1, ...}, Simproc {id = id2, ...}) = eq_procid (id1, id2);
+fun eq_simproc (Simproc {stamp = stamp1, ...}, Simproc {stamp = stamp2, ...}) = stamp1 = stamp2;
 
-fun cert_simproc thy name {lhss, proc, identifier} =
-  Simproc {name = name, lhss = map (Sign.cert_term thy) lhss, proc = proc,
-    id = (stamp (), map Thm.trim_context identifier)};
+fun cert_simproc thy name {lhss, proc} =
+  Simproc {name = name, lhss = map (Sign.cert_term thy) lhss, proc = proc, stamp = stamp ()};
 
-fun transform_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) =
+fun transform_simproc phi (Simproc {name, lhss, proc, stamp}) =
   Simproc
    {name = name,
     lhss = map (Morphism.term phi) lhss,
     proc = Morphism.transform phi proc,
-    id = (s, Morphism.fact phi ths)};
+    stamp = stamp};
 
 local
 
@@ -704,8 +699,8 @@
     (cond_warning ctxt (fn () => "Simplification procedure " ^ quote name ^ " not in simpset");
       ctxt);
 
-fun prep_procs (Simproc {name, lhss, proc, id}) =
-  lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, id = id});
+fun prep_procs (Simproc {name, lhss, proc, stamp}) =
+  lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, stamp = stamp});
 
 in
 
diff -r 745d31e63c21 -r 13252110a6fe src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/Pure/simplifier.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -36,8 +36,7 @@
   val cong_del: attribute
   val check_simproc: Proof.context -> xstring * Position.T -> string
   val the_simproc: Proof.context -> string -> simproc
-  type 'a simproc_spec =
-    {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list}
+  type 'a simproc_spec = {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option}
   val make_simproc: Proof.context -> string -> term simproc_spec -> simproc
   val define_simproc: binding -> term simproc_spec -> local_theory -> local_theory
   val define_simproc_cmd: binding -> string simproc_spec -> local_theory -> local_theory
@@ -117,25 +116,22 @@
 
 (* define simprocs *)
 
-type 'a simproc_spec =
-  {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list};
+type 'a simproc_spec = {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option};
 
-fun make_simproc ctxt name {lhss, proc, identifier} =
+fun make_simproc ctxt name {lhss, proc} =
   let
     val ctxt' = fold Variable.auto_fixes lhss ctxt;
     val lhss' = Variable.export_terms ctxt' ctxt lhss;
   in
-    cert_simproc (Proof_Context.theory_of ctxt) name
-      {lhss = lhss', proc = proc, identifier = identifier}
+    cert_simproc (Proof_Context.theory_of ctxt) name {lhss = lhss', proc = proc}
   end;
 
 local
 
-fun def_simproc prep b {lhss, proc, identifier} lthy =
+fun def_simproc prep b {lhss, proc} lthy =
   let
     val simproc =
-      make_simproc lthy (Local_Theory.full_name lthy b)
-        {lhss = prep lthy lhss, proc = proc, identifier = identifier};
+      make_simproc lthy (Local_Theory.full_name lthy b) {lhss = prep lthy lhss, proc = proc};
   in
     lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
       let
diff -r 745d31e63c21 -r 13252110a6fe src/Tools/induct.ML
--- a/src/Tools/induct.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/Tools/induct.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -173,8 +173,7 @@
 val rearrange_eqs_simproc =
   Simplifier.make_simproc @{context} "rearrange_eqs"
    {lhss = [@{term "Pure.all(t)"}],
-    proc = fn _ => fn ctxt => fn ct => mk_swap_rrule ctxt ct,
-    identifier = []};
+    proc = fn _ => fn ctxt => fn ct => mk_swap_rrule ctxt ct};
 
 
 (* rotate k premises to the left by j, skipping over first j premises *)
diff -r 745d31e63c21 -r 13252110a6fe src/ZF/Datatype_ZF.thy
--- a/src/ZF/Datatype_ZF.thy	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/ZF/Datatype_ZF.thy	Fri Apr 08 20:15:20 2016 +0200
@@ -107,7 +107,7 @@
 
   val conv =
     Simplifier.make_simproc @{context} "data_free"
-     {lhss = [@{term "(x::i) = y"}], proc = K proc, identifier = []};
+     {lhss = [@{term "(x::i) = y"}], proc = K proc};
 
 end;
 \<close>
diff -r 745d31e63c21 -r 13252110a6fe src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/ZF/arith_data.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -204,19 +204,19 @@
      [@{term "l #+ m = n"}, @{term "l = m #+ n"},
       @{term "l #* m = n"}, @{term "l = m #* n"},
       @{term "succ(m) = n"}, @{term "m = succ(n)"}],
-    proc = K EqCancelNumerals.proc, identifier = []},
+    proc = K EqCancelNumerals.proc},
   Simplifier.make_simproc @{context} "natless_cancel_numerals"
    {lhss =
      [@{term "l #+ m < n"}, @{term "l < m #+ n"},
       @{term "l #* m < n"}, @{term "l < m #* n"},
       @{term "succ(m) < n"}, @{term "m < succ(n)"}],
-    proc = K LessCancelNumerals.proc, identifier = []},
+    proc = K LessCancelNumerals.proc},
   Simplifier.make_simproc @{context} "natdiff_cancel_numerals"
    {lhss =
      [@{term "(l #+ m) #- n"}, @{term "l #- (m #+ n)"},
       @{term "(l #* m) #- n"}, @{term "l #- (m #* n)"},
       @{term "succ(m) #- n"}, @{term "m #- succ(n)"}],
-    proc = K DiffCancelNumerals.proc, identifier = []}];
+    proc = K DiffCancelNumerals.proc}];
 
 end;
 
diff -r 745d31e63c21 -r 13252110a6fe src/ZF/int_arith.ML
--- a/src/ZF/int_arith.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/ZF/int_arith.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -212,19 +212,19 @@
      [@{term "l $+ m = n"}, @{term "l = m $+ n"},
       @{term "l $- m = n"}, @{term "l = m $- n"},
       @{term "l $* m = n"}, @{term "l = m $* n"}],
-    proc = K EqCancelNumerals.proc, identifier = []},
+    proc = K EqCancelNumerals.proc},
   Simplifier.make_simproc @{context} "intless_cancel_numerals"
    {lhss =
      [@{term "l $+ m $< n"}, @{term "l $< m $+ n"},
       @{term "l $- m $< n"}, @{term "l $< m $- n"},
       @{term "l $* m $< n"}, @{term "l $< m $* n"}],
-    proc = K LessCancelNumerals.proc, identifier = []},
+    proc = K LessCancelNumerals.proc},
   Simplifier.make_simproc @{context} "intle_cancel_numerals"
    {lhss =
      [@{term "l $+ m $\<le> n"}, @{term "l $\<le> m $+ n"},
       @{term "l $- m $\<le> n"}, @{term "l $\<le> m $- n"},
       @{term "l $* m $\<le> n"}, @{term "l $\<le> m $* n"}],
-    proc = K LeCancelNumerals.proc, identifier = []}];
+    proc = K LeCancelNumerals.proc}];
 
 
 (*version without the hyps argument*)
@@ -269,7 +269,7 @@
 val combine_numerals =
   Simplifier.make_simproc @{context} "int_combine_numerals"
     {lhss = [@{term "i $+ j"}, @{term "i $- j"}],
-     proc = K CombineNumerals.proc, identifier = []};
+     proc = K CombineNumerals.proc};
 
 
 
@@ -315,7 +315,7 @@
 
 val combine_numerals_prod =
   Simplifier.make_simproc @{context} "int_combine_numerals_prod"
-   {lhss = [@{term "i $* j"}], proc = K CombineNumeralsProd.proc, identifier = []};
+   {lhss = [@{term "i $* j"}], proc = K CombineNumeralsProd.proc};
 
 end;