eliminated unused simproc identifier;
authorwenzelm
Fri Apr 08 20:15:20 2016 +0200 (2016-04-08)
changeset 6291313252110a6fe
parent 62912 745d31e63c21
child 62914 930a30c1a9af
eliminated unused simproc identifier;
src/Doc/Isar_Ref/Generic.thy
src/HOL/Decision_Procs/langford.ML
src/HOL/HOL.thy
src/HOL/HOLCF/Tools/cont_proc.ML
src/HOL/Library/Old_SMT/old_smt_real.ML
src/HOL/Library/Old_SMT/old_z3_proof_tools.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Product_Type.thy
src/HOL/Statespace/distinct_tree_prover.ML
src/HOL/Statespace/state_fun.ML
src/HOL/Statespace/state_space.ML
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/SMT/smt_real.ML
src/HOL/Tools/SMT/z3_replay_util.ML
src/HOL/Tools/groebner.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/int_arith.ML
src/HOL/Tools/numeral_simprocs.ML
src/HOL/Tools/record.ML
src/HOL/Word/WordBitwise.thy
src/Pure/Isar/isar_cmd.ML
src/Pure/ML/ml_context.ML
src/Pure/Pure.thy
src/Pure/raw_simplifier.ML
src/Pure/simplifier.ML
src/Tools/induct.ML
src/ZF/Datatype_ZF.thy
src/ZF/arith_data.ML
src/ZF/int_arith.ML
     1.1 --- a/src/Doc/Isar_Ref/Generic.thy	Thu Apr 07 22:09:23 2016 +0200
     1.2 +++ b/src/Doc/Isar_Ref/Generic.thy	Fri Apr 08 20:15:20 2016 +0200
     1.3 @@ -794,8 +794,7 @@
     1.4  
     1.5    @{rail \<open>
     1.6      @@{command simproc_setup} @{syntax name} '(' (@{syntax term} + '|') ')' '='
     1.7 -      @{syntax text} \<newline> (@'identifier' (@{syntax nameref}+))?
     1.8 -    ;
     1.9 +      @{syntax text};
    1.10  
    1.11      @@{attribute simproc} (('add' ':')? | 'del' ':') (@{syntax name}+)
    1.12    \<close>}
    1.13 @@ -810,12 +809,10 @@
    1.14    NONE} to indicate failure. The @{ML_type Proof.context} argument holds the
    1.15    full context of the current Simplifier invocation. The @{ML_type morphism}
    1.16    informs about the difference of the original compilation context wrt.\ the
    1.17 -  one of the actual application later on. The optional @{keyword "identifier"}
    1.18 -  specifies theorems that represent the logical content of the abstract theory
    1.19 -  of this simproc.
    1.20 +  one of the actual application later on.
    1.21  
    1.22 -  Morphisms and identifiers are only relevant for simprocs that are defined
    1.23 -  within a local target context, e.g.\ in a locale.
    1.24 +  Morphisms are only relevant for simprocs that are defined within a local
    1.25 +  target context, e.g.\ in a locale.
    1.26  
    1.27    \<^descr> \<open>simproc add: name\<close> and \<open>simproc del: name\<close> add or delete named simprocs
    1.28    to the current Simplifier context. The default is to add a simproc. Note
     2.1 --- a/src/HOL/Decision_Procs/langford.ML	Thu Apr 07 22:09:23 2016 +0200
     2.2 +++ b/src/HOL/Decision_Procs/langford.ML	Fri Apr 08 20:15:20 2016 +0200
     2.3 @@ -171,7 +171,7 @@
     2.4  
     2.5  val reduce_ex_simproc =
     2.6    Simplifier.make_simproc @{context} "reduce_ex_simproc"
     2.7 -    {lhss = [@{term "\<exists>x. P x"}], proc = K proc, identifier = []};
     2.8 +    {lhss = [@{term "\<exists>x. P x"}], proc = K proc};
     2.9  
    2.10  end;
    2.11  
     3.1 --- a/src/HOL/HOL.thy	Thu Apr 07 22:09:23 2016 +0200
     3.2 +++ b/src/HOL/HOL.thy	Fri Apr 08 20:15:20 2016 +0200
     3.3 @@ -1444,8 +1444,7 @@
     3.4            (case Thm.term_of ct of
     3.5              _ $ (P as _ $ @{const induct_false}) $ (_ $ Q $ _) =>
     3.6                if P <> Q then SOME Drule.swap_prems_eq else NONE
     3.7 -          | _ => NONE),
     3.8 -         identifier = []},
     3.9 +          | _ => NONE)},
    3.10         Simplifier.make_simproc @{context} "induct_equal_conj_curry"
    3.11          {lhss = [@{term "induct_conj P Q \<Longrightarrow> PROP R"}],
    3.12           proc = fn _ => fn _ => fn ct =>
    3.13 @@ -1459,8 +1458,7 @@
    3.14                    | is_conj @{const induct_false} = true
    3.15                    | is_conj _ = false
    3.16                in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
    3.17 -            | _ => NONE),
    3.18 -          identifier = []}]
    3.19 +            | _ => NONE)}]
    3.20      |> Simplifier.set_mksimps (fn ctxt =>
    3.21          Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
    3.22          map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback}))))
    3.23 @@ -1759,8 +1757,7 @@
    3.24           proc = fn _ => fn _ => fn ct =>
    3.25            (case Thm.term_of ct of
    3.26              Const (_, Type (@{type_name fun}, [Type _, _])) => SOME @{thm eq_equal}
    3.27 -          | _ => NONE),
    3.28 -         identifier = []}])
    3.29 +          | _ => NONE)}])
    3.30  \<close>
    3.31  
    3.32  
     4.1 --- a/src/HOL/HOLCF/Tools/cont_proc.ML	Thu Apr 07 22:09:23 2016 +0200
     4.2 +++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Fri Apr 08 20:15:20 2016 +0200
     4.3 @@ -127,7 +127,7 @@
     4.4  in
     4.5    val cont_proc =
     4.6      Simplifier.make_simproc @{context} "cont_proc"
     4.7 -     {lhss = [@{term "cont f"}], proc = K solve_cont, identifier = []}
     4.8 +     {lhss = [@{term "cont f"}], proc = K solve_cont}
     4.9  end
    4.10  
    4.11  val setup = map_theory_simpset (fn ctxt => ctxt addsimprocs [cont_proc])
     5.1 --- a/src/HOL/Library/Old_SMT/old_smt_real.ML	Thu Apr 07 22:09:23 2016 +0200
     5.2 +++ b/src/HOL/Library/Old_SMT/old_smt_real.ML	Fri Apr 08 20:15:20 2016 +0200
     5.3 @@ -117,7 +117,7 @@
     5.4  val real_linarith_proc =
     5.5    Simplifier.make_simproc @{context} "fast_real_arith"
     5.6     {lhss = [@{term "(m::real) < n"}, @{term "(m::real) \<le> n"}, @{term "(m::real) = n"}],
     5.7 -    proc = K Lin_Arith.simproc, identifier = []}
     5.8 +    proc = K Lin_Arith.simproc}
     5.9  
    5.10  
    5.11  (* setup *)
     6.1 --- a/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML	Thu Apr 07 22:09:23 2016 +0200
     6.2 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML	Fri Apr 08 20:15:20 2016 +0200
     6.3 @@ -345,13 +345,13 @@
     6.4        addsimprocs [
     6.5          Simplifier.make_simproc @{context} "fast_int_arith"
     6.6           {lhss = [@{term "(m::int) < n"}, @{term "(m::int) \<le> n"}, @{term "(m::int) = n"}],
     6.7 -          proc = K Lin_Arith.simproc, identifier = []},
     6.8 +          proc = K Lin_Arith.simproc},
     6.9          Simplifier.make_simproc @{context} "antisym_le"
    6.10           {lhss = [@{term "(x::'a::order) \<le> y"}],
    6.11 -          proc = K prove_antisym_le, identifier = []},
    6.12 +          proc = K prove_antisym_le},
    6.13          Simplifier.make_simproc @{context} "antisym_less"
    6.14           {lhss = [@{term "\<not> (x::'a::linorder) < y"}],
    6.15 -          proc = K prove_antisym_less, identifier = []}])
    6.16 +          proc = K prove_antisym_less}])
    6.17  
    6.18    structure Simpset = Generic_Data
    6.19    (
     7.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Thu Apr 07 22:09:23 2016 +0200
     7.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Apr 08 20:15:20 2016 +0200
     7.3 @@ -122,7 +122,7 @@
     7.4  
     7.5  val perm_simproc =
     7.6    Simplifier.make_simproc @{context} "perm_simp"
     7.7 -   {lhss = [@{term "pi1 \<bullet> (pi2 \<bullet> x)"}], proc = K perm_simproc', identifier = []};
     7.8 +   {lhss = [@{term "pi1 \<bullet> (pi2 \<bullet> x)"}], proc = K perm_simproc'};
     7.9  
    7.10  fun projections ctxt rule =
    7.11    Project_Rule.projections ctxt rule
     8.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Thu Apr 07 22:09:23 2016 +0200
     8.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Apr 08 20:15:20 2016 +0200
     8.3 @@ -47,8 +47,7 @@
     8.4          Const (@{const_name Nominal.perm}, _) $ _ $ t =>
     8.5            if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
     8.6            then SOME perm_bool else NONE
     8.7 -      | _ => NONE),
     8.8 -    identifier = []};
     8.9 +      | _ => NONE)};
    8.10  
    8.11  fun transp ([] :: _) = []
    8.12    | transp xs = map hd xs :: transp (map tl xs);
     9.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Thu Apr 07 22:09:23 2016 +0200
     9.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Apr 08 20:15:20 2016 +0200
     9.3 @@ -51,8 +51,7 @@
     9.4          Const (@{const_name Nominal.perm}, _) $ _ $ t =>
     9.5            if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
     9.6            then SOME perm_bool else NONE
     9.7 -       | _ => NONE),
     9.8 -    identifier = []};
     9.9 +       | _ => NONE)};
    9.10  
    9.11  fun transp ([] :: _) = []
    9.12    | transp xs = map hd xs :: transp (map tl xs);
    10.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Thu Apr 07 22:09:23 2016 +0200
    10.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Fri Apr 08 20:15:20 2016 +0200
    10.3 @@ -114,7 +114,7 @@
    10.4  
    10.5  val perm_simproc_app =
    10.6    Simplifier.make_simproc @{context} "perm_simproc_app"
    10.7 -   {lhss = [@{term "Nominal.perm pi x"}], proc = K perm_simproc_app', identifier = []}
    10.8 +   {lhss = [@{term "Nominal.perm pi x"}], proc = K perm_simproc_app'}
    10.9  
   10.10  (* a simproc that deals with permutation instances in front of functions  *)
   10.11  fun perm_simproc_fun' ctxt ct =
   10.12 @@ -136,7 +136,7 @@
   10.13  
   10.14  val perm_simproc_fun =
   10.15    Simplifier.make_simproc @{context} "perm_simproc_fun"
   10.16 -   {lhss = [@{term "Nominal.perm pi x"}], proc = K perm_simproc_fun', identifier = []}
   10.17 +   {lhss = [@{term "Nominal.perm pi x"}], proc = K perm_simproc_fun'}
   10.18  
   10.19  (* function for simplyfying permutations          *)
   10.20  (* stac contains the simplifiation tactic that is *)
   10.21 @@ -219,7 +219,7 @@
   10.22  val perm_compose_simproc =
   10.23    Simplifier.make_simproc @{context} "perm_compose"
   10.24     {lhss = [@{term "Nominal.perm pi1 (Nominal.perm pi2 t)"}],
   10.25 -    proc = K perm_compose_simproc', identifier = []}
   10.26 +    proc = K perm_compose_simproc'}
   10.27  
   10.28  fun perm_compose_tac ctxt i =
   10.29    ("analysing permutation compositions on the lhs",
    11.1 --- a/src/HOL/Product_Type.thy	Thu Apr 07 22:09:23 2016 +0200
    11.2 +++ b/src/HOL/Product_Type.thy	Fri Apr 08 20:15:20 2016 +0200
    11.3 @@ -1327,8 +1327,7 @@
    11.4    Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs
    11.5      [Simplifier.make_simproc @{context} "set comprehension"
    11.6        {lhss = [@{term "Collect P"}],
    11.7 -       proc = K Set_Comprehension_Pointfree.code_simproc,
    11.8 -       identifier = []}])
    11.9 +       proc = K Set_Comprehension_Pointfree.code_simproc}])
   11.10  \<close>
   11.11  
   11.12  
    12.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Thu Apr 07 22:09:23 2016 +0200
    12.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Fri Apr 08 20:15:20 2016 +0200
    12.3 @@ -360,8 +360,7 @@
    12.4          Const (@{const_name HOL.eq}, _) $ x $ y =>
    12.5            Option.map (fn neq => @{thm neq_to_eq_False} OF [neq])
    12.6              (get_fst_success (neq_x_y ctxt x y) names)
    12.7 -      | _ => NONE),
    12.8 -    identifier = []};
    12.9 +      | _ => NONE)};
   12.10  
   12.11  end;
   12.12  
    13.1 --- a/src/HOL/Statespace/state_fun.ML	Thu Apr 07 22:09:23 2016 +0200
    13.2 +++ b/src/HOL/Statespace/state_fun.ML	Fri Apr 08 20:15:20 2016 +0200
    13.3 @@ -72,8 +72,7 @@
    13.4                  else SOME (conj_cong OF [P_P', Q_Q'])
    13.5                end
    13.6             end
    13.7 -      | _ => NONE),
    13.8 -    identifier = []};
    13.9 +      | _ => NONE)};
   13.10  
   13.11  fun string_eq_simp_tac ctxt =
   13.12    simp_tac (put_simpset HOL_basic_ss ctxt
   13.13 @@ -154,8 +153,7 @@
   13.14            else SOME thm
   13.15          end
   13.16          handle Option.Option => NONE)
   13.17 -      | _ => NONE),
   13.18 -  identifier = []};
   13.19 +      | _ => NONE)};
   13.20  
   13.21  
   13.22  local
   13.23 @@ -260,8 +258,7 @@
   13.24                  in SOME (Thm.transitive eq1 eq2) end
   13.25              | _ => NONE)
   13.26            end
   13.27 -      | _ => NONE),
   13.28 -  identifier = []};
   13.29 +      | _ => NONE)};
   13.30  
   13.31  end;
   13.32  
   13.33 @@ -326,8 +323,7 @@
   13.34                val thm' = if swap then swap_ex_eq OF [thm] else thm
   13.35              in SOME thm' end handle TERM _ => NONE)
   13.36          | _ => NONE)
   13.37 -      end handle Option.Option => NONE,
   13.38 -  identifier = []};
   13.39 +      end handle Option.Option => NONE};
   13.40  
   13.41  end;
   13.42  
    14.1 --- a/src/HOL/Statespace/state_space.ML	Thu Apr 07 22:09:23 2016 +0200
    14.2 +++ b/src/HOL/Statespace/state_space.ML	Fri Apr 08 20:15:20 2016 +0200
    14.3 @@ -218,8 +218,7 @@
    14.4          Const (@{const_name HOL.eq},_) $ (x as Free _) $ (y as Free _) =>
    14.5            Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq])
    14.6              (neq_x_y ctxt x y)
    14.7 -      | _ => NONE),
    14.8 -    identifier = []};
    14.9 +      | _ => NONE)};
   14.10  
   14.11  fun interprete_parent name dist_thm_name parent_expr thy =
   14.12    let
    15.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Apr 07 22:09:23 2016 +0200
    15.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Apr 08 20:15:20 2016 +0200
    15.3 @@ -150,8 +150,7 @@
    15.4  val regularize_simproc =
    15.5    Simplifier.make_simproc @{context} "regularize"
    15.6      {lhss = [@{term "Ball (Respects (R1 ===> R2)) P"}, @{term "Bex (Respects (R1 ===> R2)) P"}],
    15.7 -     proc = K ball_bex_range_simproc,
    15.8 -     identifier = []};
    15.9 +     proc = K ball_bex_range_simproc};
   15.10  
   15.11  fun regularize_tac ctxt =
   15.12    let
    16.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Thu Apr 07 22:09:23 2016 +0200
    16.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Fri Apr 08 20:15:20 2016 +0200
    16.3 @@ -101,7 +101,7 @@
    16.4  val real_linarith_proc =
    16.5    Simplifier.make_simproc @{context} "fast_real_arith"
    16.6     {lhss = [@{term "(m::real) < n"}, @{term "(m::real) \<le> n"}, @{term "(m::real) = n"}],
    16.7 -    proc = K Lin_Arith.simproc, identifier = []}
    16.8 +    proc = K Lin_Arith.simproc}
    16.9  
   16.10  
   16.11  (* setup *)
    17.1 --- a/src/HOL/Tools/SMT/z3_replay_util.ML	Thu Apr 07 22:09:23 2016 +0200
    17.2 +++ b/src/HOL/Tools/SMT/z3_replay_util.ML	Fri Apr 08 20:15:20 2016 +0200
    17.3 @@ -126,13 +126,13 @@
    17.4        addsimprocs [@{simproc numeral_divmod},
    17.5          Simplifier.make_simproc @{context} "fast_int_arith"
    17.6           {lhss = [@{term "(m::int) < n"}, @{term "(m::int) \<le> n"}, @{term "(m::int) = n"}],
    17.7 -          proc = K Lin_Arith.simproc, identifier = []},
    17.8 +          proc = K Lin_Arith.simproc},
    17.9          Simplifier.make_simproc @{context} "antisym_le"
   17.10           {lhss = [@{term "(x::'a::order) \<le> y"}],
   17.11 -          proc = K prove_antisym_le, identifier = []},
   17.12 +          proc = K prove_antisym_le},
   17.13          Simplifier.make_simproc @{context} "antisym_less"
   17.14           {lhss = [@{term "\<not> (x::'a::linorder) < y"}],
   17.15 -          proc = K prove_antisym_less, identifier = []}])
   17.16 +          proc = K prove_antisym_less}])
   17.17  
   17.18    structure Simpset = Generic_Data
   17.19    (
    18.1 --- a/src/HOL/Tools/groebner.ML	Thu Apr 07 22:09:23 2016 +0200
    18.2 +++ b/src/HOL/Tools/groebner.ML	Fri Apr 08 20:15:20 2016 +0200
    18.3 @@ -787,7 +787,7 @@
    18.4    in
    18.5      Simplifier.cert_simproc (Thm.theory_of_thm idl_sub) "poly_eq_simproc"
    18.6       {lhss = [Thm.term_of (Thm.lhs_of idl_sub)],
    18.7 -      proc = fn _ => fn _ => proc, identifier = []}
    18.8 +      proc = fn _ => fn _ => proc}
    18.9    end;
   18.10  
   18.11  val poly_eq_ss =
    19.1 --- a/src/HOL/Tools/inductive_set.ML	Thu Apr 07 22:09:23 2016 +0200
    19.2 +++ b/src/HOL/Tools/inductive_set.ML	Fri Apr 08 20:15:20 2016 +0200
    19.3 @@ -98,8 +98,7 @@
    19.4                end
    19.5              else NONE
    19.6          | _ => NONE)
    19.7 -      end,
    19.8 -    identifier = []};
    19.9 +      end};
   19.10  
   19.11  (* only eta contract terms occurring as arguments of functions satisfying p *)
   19.12  fun eta_contract p =
   19.13 @@ -319,8 +318,7 @@
   19.14        {lhss = [anyt],
   19.15         proc = fn _ => fn ctxt => fn ct =>
   19.16          lookup_rule (Proof_Context.theory_of ctxt)
   19.17 -          (Thm.prop_of #> Logic.dest_equals) rules' (Thm.term_of ct),
   19.18 -       identifier = []}
   19.19 +          (Thm.prop_of #> Logic.dest_equals) rules' (Thm.term_of ct)}
   19.20    end;
   19.21  
   19.22  fun to_pred_proc thy rules t =
    20.1 --- a/src/HOL/Tools/int_arith.ML	Thu Apr 07 22:09:23 2016 +0200
    20.2 +++ b/src/HOL/Tools/int_arith.ML	Fri Apr 08 20:15:20 2016 +0200
    20.3 @@ -29,8 +29,7 @@
    20.4        let val T = Thm.ctyp_of_cterm ct in
    20.5          if Thm.typ_of T = @{typ int} then NONE
    20.6          else SOME (Thm.instantiate' [SOME T] [] zeroth)
    20.7 -      end,
    20.8 -     identifier = []};
    20.9 +      end};
   20.10  
   20.11  val oneth = Thm.symmetric (mk_meta_eq @{thm of_int_1});
   20.12  
   20.13 @@ -41,8 +40,7 @@
   20.14        let val T = Thm.ctyp_of_cterm ct in
   20.15          if Thm.typ_of T = @{typ int} then NONE
   20.16          else SOME (Thm.instantiate' [SOME T] [] oneth)
   20.17 -      end,
   20.18 -    identifier = []};
   20.19 +      end};
   20.20  
   20.21  fun check (Const (@{const_name Groups.one}, @{typ int})) = false
   20.22    | check (Const (@{const_name Groups.one}, _)) = true
   20.23 @@ -71,8 +69,7 @@
   20.24      proc = fn _ => fn ctxt => fn ct =>
   20.25        if check (Thm.term_of ct)
   20.26        then SOME (Simplifier.rewrite (put_simpset conv_ss ctxt) ct)
   20.27 -      else NONE,
   20.28 -    identifier = []};
   20.29 +      else NONE};
   20.30  
   20.31  
   20.32  fun number_of ctxt T n =
    21.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Thu Apr 07 22:09:23 2016 +0200
    21.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Fri Apr 08 20:15:20 2016 +0200
    21.3 @@ -451,16 +451,14 @@
    21.4        @{term "((numeral v)::'a::field) / (- numeral w)"},
    21.5        @{term "((- numeral v)::'a::field) / (numeral w)"},
    21.6        @{term "((- numeral v)::'a::field) / (- numeral w)"}],
    21.7 -    proc = K DivideCancelNumeralFactor.proc,
    21.8 -    identifier = []}
    21.9 +    proc = K DivideCancelNumeralFactor.proc}
   21.10  
   21.11  val field_cancel_numeral_factors =
   21.12    [Simplifier.make_simproc @{context} "field_eq_cancel_numeral_factor"
   21.13      {lhss =
   21.14         [@{term "(l::'a::field) * m = n"},
   21.15          @{term "(l::'a::field) = m * n"}],
   21.16 -      proc = K EqCancelNumeralFactor.proc,
   21.17 -      identifier = []},
   21.18 +      proc = K EqCancelNumeralFactor.proc},
   21.19     field_divide_cancel_numeral_factor]
   21.20  
   21.21  
   21.22 @@ -693,12 +691,12 @@
   21.23  val add_frac_frac_simproc =
   21.24    Simplifier.make_simproc @{context} "add_frac_frac_simproc"
   21.25     {lhss = [@{term "(x::'a::field) / y + (w::'a::field) / z"}],
   21.26 -    proc = K proc, identifier = []}
   21.27 +    proc = K proc}
   21.28  
   21.29  val add_frac_num_simproc =
   21.30    Simplifier.make_simproc @{context} "add_frac_num_simproc"
   21.31     {lhss = [@{term "(x::'a::field) / y + z"}, @{term "z + (x::'a::field) / y"}],
   21.32 -    proc = K proc2, identifier = []}
   21.33 +    proc = K proc2}
   21.34  
   21.35  val ord_frac_simproc =
   21.36    Simplifier.make_simproc @{context} "ord_frac_simproc"
   21.37 @@ -709,7 +707,7 @@
   21.38        @{term "c \<le> (a::'a::{field,ord}) / b"},
   21.39        @{term "c = (a::'a::{field,ord}) / b"},
   21.40        @{term "(a::'a::{field, ord}) / b = c"}],
   21.41 -    proc = K proc3, identifier = []}
   21.42 +    proc = K proc3}
   21.43  
   21.44  val ths =
   21.45   [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
    22.1 --- a/src/HOL/Tools/record.ML	Thu Apr 07 22:09:23 2016 +0200
    22.2 +++ b/src/HOL/Tools/record.ML	Fri Apr 08 20:15:20 2016 +0200
    22.3 @@ -1116,8 +1116,7 @@
    22.4                end
    22.5              else NONE
    22.6          | _ => NONE)
    22.7 -      end,
    22.8 -    identifier = []};
    22.9 +      end};
   22.10  
   22.11  fun get_upd_acc_cong_thm upd acc thy ss =
   22.12    let
   22.13 @@ -1250,8 +1249,7 @@
   22.14              (prove_unfold_defs thy noops' [simproc]
   22.15                (Logic.list_all (vars, Logic.mk_equals (lhs, rhs))))
   22.16          else NONE
   22.17 -      end,
   22.18 -    identifier = []};
   22.19 +      end};
   22.20  
   22.21  end;
   22.22  
   22.23 @@ -1282,8 +1280,7 @@
   22.24                (case get_equalities (Proof_Context.theory_of ctxt) name of
   22.25                  NONE => NONE
   22.26                | SOME thm => SOME (thm RS @{thm Eq_TrueI})))
   22.27 -      | _ => NONE),
   22.28 -    identifier = []};
   22.29 +      | _ => NONE)};
   22.30  
   22.31  
   22.32  (* split_simproc *)
   22.33 @@ -1320,8 +1317,7 @@
   22.34                    else NONE
   22.35                  end)
   22.36            else NONE
   22.37 -      | _ => NONE),
   22.38 -    identifier = []};
   22.39 +      | _ => NONE)};
   22.40  
   22.41  val ex_sel_eq_simproc =
   22.42    Simplifier.make_simproc @{context} "ex_sel_eq"
   22.43 @@ -1362,8 +1358,7 @@
   22.44                      addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1))
   22.45              end handle TERM _ => NONE)
   22.46          | _ => NONE)
   22.47 -      end,
   22.48 -    identifier = []};
   22.49 +      end};
   22.50  
   22.51  
   22.52  (* split_simp_tac *)
    23.1 --- a/src/HOL/Word/WordBitwise.thy	Thu Apr 07 22:09:23 2016 +0200
    23.2 +++ b/src/HOL/Word/WordBitwise.thy	Fri Apr 08 20:15:20 2016 +0200
    23.3 @@ -525,7 +525,7 @@
    23.4  
    23.5  val expand_upt_simproc =
    23.6    Simplifier.make_simproc @{context} "expand_upt"
    23.7 -   {lhss = [@{term "upt x y"}], proc = K upt_conv, identifier = []};
    23.8 +   {lhss = [@{term "upt x y"}], proc = K upt_conv};
    23.9  
   23.10  fun word_len_simproc_fn ctxt ct =
   23.11    case Thm.term_of ct of
   23.12 @@ -541,7 +541,7 @@
   23.13  
   23.14  val word_len_simproc =
   23.15    Simplifier.make_simproc @{context} "word_len"
   23.16 -   {lhss = [@{term "len_of x"}], proc = K word_len_simproc_fn, identifier = []};
   23.17 +   {lhss = [@{term "len_of x"}], proc = K word_len_simproc_fn};
   23.18  
   23.19  (* convert 5 or nat 5 to Suc 4 when n_sucs = 1, Suc (Suc 4) when n_sucs = 2,
   23.20     or just 5 (discarding nat) when n_sucs = 0 *)
   23.21 @@ -568,7 +568,7 @@
   23.22  fun nat_get_Suc_simproc n_sucs ts =
   23.23    Simplifier.make_simproc @{context} "nat_get_Suc"
   23.24     {lhss = map (fn t => t $ @{term "n :: nat"}) ts,
   23.25 -    proc = K (nat_get_Suc_simproc_fn n_sucs), identifier = []};
   23.26 +    proc = K (nat_get_Suc_simproc_fn n_sucs)};
   23.27  
   23.28  val no_split_ss =
   23.29    simpset_of (put_simpset HOL_ss @{context}
    24.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Apr 07 22:09:23 2016 +0200
    24.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Apr 08 20:15:20 2016 +0200
    24.3 @@ -18,7 +18,7 @@
    24.4    val oracle: bstring * Position.range -> Input.source -> theory -> theory
    24.5    val declaration: {syntax: bool, pervasive: bool} -> Input.source -> local_theory -> local_theory
    24.6    val simproc_setup: string * Position.T -> string list -> Input.source ->
    24.7 -    string list -> local_theory -> local_theory
    24.8 +    local_theory -> local_theory
    24.9    val qed: Method.text_range option -> Toplevel.transition -> Toplevel.transition
   24.10    val terminal_proof: Method.text_range * Method.text_range option ->
   24.11      Toplevel.transition -> Toplevel.transition
   24.12 @@ -151,14 +151,13 @@
   24.13  
   24.14  (* simprocs *)
   24.15  
   24.16 -fun simproc_setup name lhss source identifier =
   24.17 +fun simproc_setup name lhss source =
   24.18    ML_Lex.read_source false source
   24.19    |> ML_Context.expression (Input.range_of source) "proc"
   24.20      "Morphism.morphism -> Proof.context -> cterm -> thm option"
   24.21      ("Context.map_proof (Simplifier.define_simproc_cmd " ^
   24.22        ML_Syntax.atomic (ML_Syntax.make_binding name) ^
   24.23 -      "{lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
   24.24 -      \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})")
   24.25 +      "{lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc})")
   24.26    |> Context.proof_map;
   24.27  
   24.28  
    25.1 --- a/src/Pure/ML/ml_context.ML	Thu Apr 07 22:09:23 2016 +0200
    25.2 +++ b/src/Pure/ML/ml_context.ML	Fri Apr 08 20:15:20 2016 +0200
    25.3 @@ -6,9 +6,6 @@
    25.4  
    25.5  signature ML_CONTEXT =
    25.6  sig
    25.7 -  val thm: xstring -> thm
    25.8 -  val thms: xstring -> thm list
    25.9 -  val exec: (unit -> unit) -> Context.generic -> Context.generic
   25.10    val check_antiquotation: Proof.context -> xstring * Position.T -> string
   25.11    val struct_name: Proof.context -> string
   25.12    val variant: string -> Proof.context -> string * Proof.context
   25.13 @@ -23,6 +20,7 @@
   25.14    val eval_in: Proof.context option -> ML_Compiler.flags -> Position.T ->
   25.15      ML_Lex.token Antiquote.antiquote list -> unit
   25.16    val eval_source_in: Proof.context option -> ML_Compiler.flags -> Input.source -> unit
   25.17 +  val exec: (unit -> unit) -> Context.generic -> Context.generic
   25.18    val expression: Position.range -> string -> string -> string ->
   25.19      ML_Lex.token Antiquote.antiquote list -> Context.generic -> Context.generic
   25.20  end
   25.21 @@ -30,19 +28,6 @@
   25.22  structure ML_Context: ML_CONTEXT =
   25.23  struct
   25.24  
   25.25 -(** implicit ML context **)
   25.26 -
   25.27 -fun thm name = Proof_Context.get_thm (Context.the_local_context ()) name;
   25.28 -fun thms name = Proof_Context.get_thms (Context.the_local_context ()) name;
   25.29 -
   25.30 -fun exec (e: unit -> unit) context =
   25.31 -  (case Context.setmp_generic_context (SOME context)
   25.32 -      (fn () => (e (); Context.get_generic_context ())) () of
   25.33 -    SOME context' => context'
   25.34 -  | NONE => error "Missing context after execution");
   25.35 -
   25.36 -
   25.37 -
   25.38  (** ML antiquotations **)
   25.39  
   25.40  (* names for generated environment *)
   25.41 @@ -220,6 +205,12 @@
   25.42    Context.setmp_generic_context (Option.map Context.Proof ctxt)
   25.43      (fn () => eval_source flags source) ();
   25.44  
   25.45 +fun exec (e: unit -> unit) context =
   25.46 +  (case Context.setmp_generic_context (SOME context)
   25.47 +      (fn () => (e (); Context.get_generic_context ())) () of
   25.48 +    SOME context' => context'
   25.49 +  | NONE => error "Missing context after execution");
   25.50 +
   25.51  fun expression range name constraint body ants =
   25.52    exec (fn () =>
   25.53      eval ML_Compiler.flags (#1 range)
    26.1 --- a/src/Pure/Pure.thy	Thu Apr 07 22:09:23 2016 +0200
    26.2 +++ b/src/Pure/Pure.thy	Fri Apr 08 20:15:20 2016 +0200
    26.3 @@ -9,7 +9,7 @@
    26.4      "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>"
    26.5      "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
    26.6      "\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
    26.7 -    "defines" "rewrites" "fixes" "for" "identifier" "if" "in" "includes" "infix"
    26.8 +    "defines" "rewrites" "fixes" "for" "if" "in" "includes" "infix"
    26.9      "infixl" "infixr" "is" "notes" "obtains" "open" "output"
   26.10      "overloaded" "pervasive" "premises" "private" "qualified" "rewrites"
   26.11      "shows" "structure" "unchecked" "where" "when" "|"
   26.12 @@ -210,8 +210,7 @@
   26.13    Outer_Syntax.local_theory @{command_keyword simproc_setup} "define simproc in ML"
   26.14      (Parse.position Parse.name --
   26.15        (@{keyword "("} |-- Parse.enum1 "|" Parse.term --| @{keyword ")"} --| @{keyword "="}) --
   26.16 -      Parse.ML_source -- Scan.optional (@{keyword "identifier"} |-- Scan.repeat1 Parse.xname) []
   26.17 -    >> (fn (((a, b), c), d) => Isar_Cmd.simproc_setup a b c d));
   26.18 +      Parse.ML_source >> (fn ((a, b), c) => Isar_Cmd.simproc_setup a b c));
   26.19  
   26.20  in end\<close>
   26.21  
    27.1 --- a/src/Pure/raw_simplifier.ML	Thu Apr 07 22:09:23 2016 +0200
    27.2 +++ b/src/Pure/raw_simplifier.ML	Fri Apr 08 20:15:20 2016 +0200
    27.3 @@ -36,8 +36,7 @@
    27.4    type simproc
    27.5    val eq_simproc: simproc * simproc -> bool
    27.6    val cert_simproc: theory -> string ->
    27.7 -    {lhss: term list, proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list}
    27.8 -    -> simproc
    27.9 +    {lhss: term list, proc: morphism -> Proof.context -> cterm -> thm option} -> simproc
   27.10    val transform_simproc: morphism -> simproc -> simproc
   27.11    val simpset_of: Proof.context -> simpset
   27.12    val put_simpset: simpset -> Proof.context -> Proof.context
   27.13 @@ -220,12 +219,9 @@
   27.14     {name: string,
   27.15      lhs: term,
   27.16      proc: Proof.context -> cterm -> thm option,
   27.17 -    id: stamp * thm list};
   27.18 +    stamp: stamp};
   27.19  
   27.20 -fun eq_procid ((s1: stamp, ths1: thm list), (s2, ths2)) =
   27.21 -  s1 = s2 andalso eq_list Thm.eq_thm (ths1, ths2);
   27.22 -
   27.23 -fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = eq_procid (id1, id2);
   27.24 +fun eq_proc (Proc {stamp = stamp1, ...}, Proc {stamp = stamp2, ...}) = stamp1 = stamp2;
   27.25  
   27.26  
   27.27  (* solvers *)
   27.28 @@ -298,8 +294,8 @@
   27.29   {simps = Net.entries rules
   27.30      |> map (fn {name, thm, ...} => (name, thm)),
   27.31    procs = Net.entries procs
   27.32 -    |> map (fn Proc {name, lhs, id, ...} => ((name, lhs), id))
   27.33 -    |> partition_eq (eq_snd eq_procid)
   27.34 +    |> map (fn Proc {name, lhs, stamp, ...} => ((name, lhs), stamp))
   27.35 +    |> partition_eq (eq_snd op =)
   27.36      |> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)),
   27.37    congs = #1 congs,
   27.38    weak_congs = #2 congs,
   27.39 @@ -667,20 +663,19 @@
   27.40      {name: string,
   27.41       lhss: term list,
   27.42       proc: morphism -> Proof.context -> cterm -> thm option,
   27.43 -     id: stamp * thm list};
   27.44 +     stamp: stamp};
   27.45  
   27.46 -fun eq_simproc (Simproc {id = id1, ...}, Simproc {id = id2, ...}) = eq_procid (id1, id2);
   27.47 +fun eq_simproc (Simproc {stamp = stamp1, ...}, Simproc {stamp = stamp2, ...}) = stamp1 = stamp2;
   27.48  
   27.49 -fun cert_simproc thy name {lhss, proc, identifier} =
   27.50 -  Simproc {name = name, lhss = map (Sign.cert_term thy) lhss, proc = proc,
   27.51 -    id = (stamp (), map Thm.trim_context identifier)};
   27.52 +fun cert_simproc thy name {lhss, proc} =
   27.53 +  Simproc {name = name, lhss = map (Sign.cert_term thy) lhss, proc = proc, stamp = stamp ()};
   27.54  
   27.55 -fun transform_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) =
   27.56 +fun transform_simproc phi (Simproc {name, lhss, proc, stamp}) =
   27.57    Simproc
   27.58     {name = name,
   27.59      lhss = map (Morphism.term phi) lhss,
   27.60      proc = Morphism.transform phi proc,
   27.61 -    id = (s, Morphism.fact phi ths)};
   27.62 +    stamp = stamp};
   27.63  
   27.64  local
   27.65  
   27.66 @@ -704,8 +699,8 @@
   27.67      (cond_warning ctxt (fn () => "Simplification procedure " ^ quote name ^ " not in simpset");
   27.68        ctxt);
   27.69  
   27.70 -fun prep_procs (Simproc {name, lhss, proc, id}) =
   27.71 -  lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, id = id});
   27.72 +fun prep_procs (Simproc {name, lhss, proc, stamp}) =
   27.73 +  lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, stamp = stamp});
   27.74  
   27.75  in
   27.76  
    28.1 --- a/src/Pure/simplifier.ML	Thu Apr 07 22:09:23 2016 +0200
    28.2 +++ b/src/Pure/simplifier.ML	Fri Apr 08 20:15:20 2016 +0200
    28.3 @@ -36,8 +36,7 @@
    28.4    val cong_del: attribute
    28.5    val check_simproc: Proof.context -> xstring * Position.T -> string
    28.6    val the_simproc: Proof.context -> string -> simproc
    28.7 -  type 'a simproc_spec =
    28.8 -    {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list}
    28.9 +  type 'a simproc_spec = {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option}
   28.10    val make_simproc: Proof.context -> string -> term simproc_spec -> simproc
   28.11    val define_simproc: binding -> term simproc_spec -> local_theory -> local_theory
   28.12    val define_simproc_cmd: binding -> string simproc_spec -> local_theory -> local_theory
   28.13 @@ -117,25 +116,22 @@
   28.14  
   28.15  (* define simprocs *)
   28.16  
   28.17 -type 'a simproc_spec =
   28.18 -  {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list};
   28.19 +type 'a simproc_spec = {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option};
   28.20  
   28.21 -fun make_simproc ctxt name {lhss, proc, identifier} =
   28.22 +fun make_simproc ctxt name {lhss, proc} =
   28.23    let
   28.24      val ctxt' = fold Variable.auto_fixes lhss ctxt;
   28.25      val lhss' = Variable.export_terms ctxt' ctxt lhss;
   28.26    in
   28.27 -    cert_simproc (Proof_Context.theory_of ctxt) name
   28.28 -      {lhss = lhss', proc = proc, identifier = identifier}
   28.29 +    cert_simproc (Proof_Context.theory_of ctxt) name {lhss = lhss', proc = proc}
   28.30    end;
   28.31  
   28.32  local
   28.33  
   28.34 -fun def_simproc prep b {lhss, proc, identifier} lthy =
   28.35 +fun def_simproc prep b {lhss, proc} lthy =
   28.36    let
   28.37      val simproc =
   28.38 -      make_simproc lthy (Local_Theory.full_name lthy b)
   28.39 -        {lhss = prep lthy lhss, proc = proc, identifier = identifier};
   28.40 +      make_simproc lthy (Local_Theory.full_name lthy b) {lhss = prep lthy lhss, proc = proc};
   28.41    in
   28.42      lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
   28.43        let
    29.1 --- a/src/Tools/induct.ML	Thu Apr 07 22:09:23 2016 +0200
    29.2 +++ b/src/Tools/induct.ML	Fri Apr 08 20:15:20 2016 +0200
    29.3 @@ -173,8 +173,7 @@
    29.4  val rearrange_eqs_simproc =
    29.5    Simplifier.make_simproc @{context} "rearrange_eqs"
    29.6     {lhss = [@{term "Pure.all(t)"}],
    29.7 -    proc = fn _ => fn ctxt => fn ct => mk_swap_rrule ctxt ct,
    29.8 -    identifier = []};
    29.9 +    proc = fn _ => fn ctxt => fn ct => mk_swap_rrule ctxt ct};
   29.10  
   29.11  
   29.12  (* rotate k premises to the left by j, skipping over first j premises *)
    30.1 --- a/src/ZF/Datatype_ZF.thy	Thu Apr 07 22:09:23 2016 +0200
    30.2 +++ b/src/ZF/Datatype_ZF.thy	Fri Apr 08 20:15:20 2016 +0200
    30.3 @@ -107,7 +107,7 @@
    30.4  
    30.5    val conv =
    30.6      Simplifier.make_simproc @{context} "data_free"
    30.7 -     {lhss = [@{term "(x::i) = y"}], proc = K proc, identifier = []};
    30.8 +     {lhss = [@{term "(x::i) = y"}], proc = K proc};
    30.9  
   30.10  end;
   30.11  \<close>
    31.1 --- a/src/ZF/arith_data.ML	Thu Apr 07 22:09:23 2016 +0200
    31.2 +++ b/src/ZF/arith_data.ML	Fri Apr 08 20:15:20 2016 +0200
    31.3 @@ -204,19 +204,19 @@
    31.4       [@{term "l #+ m = n"}, @{term "l = m #+ n"},
    31.5        @{term "l #* m = n"}, @{term "l = m #* n"},
    31.6        @{term "succ(m) = n"}, @{term "m = succ(n)"}],
    31.7 -    proc = K EqCancelNumerals.proc, identifier = []},
    31.8 +    proc = K EqCancelNumerals.proc},
    31.9    Simplifier.make_simproc @{context} "natless_cancel_numerals"
   31.10     {lhss =
   31.11       [@{term "l #+ m < n"}, @{term "l < m #+ n"},
   31.12        @{term "l #* m < n"}, @{term "l < m #* n"},
   31.13        @{term "succ(m) < n"}, @{term "m < succ(n)"}],
   31.14 -    proc = K LessCancelNumerals.proc, identifier = []},
   31.15 +    proc = K LessCancelNumerals.proc},
   31.16    Simplifier.make_simproc @{context} "natdiff_cancel_numerals"
   31.17     {lhss =
   31.18       [@{term "(l #+ m) #- n"}, @{term "l #- (m #+ n)"},
   31.19        @{term "(l #* m) #- n"}, @{term "l #- (m #* n)"},
   31.20        @{term "succ(m) #- n"}, @{term "m #- succ(n)"}],
   31.21 -    proc = K DiffCancelNumerals.proc, identifier = []}];
   31.22 +    proc = K DiffCancelNumerals.proc}];
   31.23  
   31.24  end;
   31.25  
    32.1 --- a/src/ZF/int_arith.ML	Thu Apr 07 22:09:23 2016 +0200
    32.2 +++ b/src/ZF/int_arith.ML	Fri Apr 08 20:15:20 2016 +0200
    32.3 @@ -212,19 +212,19 @@
    32.4       [@{term "l $+ m = n"}, @{term "l = m $+ n"},
    32.5        @{term "l $- m = n"}, @{term "l = m $- n"},
    32.6        @{term "l $* m = n"}, @{term "l = m $* n"}],
    32.7 -    proc = K EqCancelNumerals.proc, identifier = []},
    32.8 +    proc = K EqCancelNumerals.proc},
    32.9    Simplifier.make_simproc @{context} "intless_cancel_numerals"
   32.10     {lhss =
   32.11       [@{term "l $+ m $< n"}, @{term "l $< m $+ n"},
   32.12        @{term "l $- m $< n"}, @{term "l $< m $- n"},
   32.13        @{term "l $* m $< n"}, @{term "l $< m $* n"}],
   32.14 -    proc = K LessCancelNumerals.proc, identifier = []},
   32.15 +    proc = K LessCancelNumerals.proc},
   32.16    Simplifier.make_simproc @{context} "intle_cancel_numerals"
   32.17     {lhss =
   32.18       [@{term "l $+ m $\<le> n"}, @{term "l $\<le> m $+ n"},
   32.19        @{term "l $- m $\<le> n"}, @{term "l $\<le> m $- n"},
   32.20        @{term "l $* m $\<le> n"}, @{term "l $\<le> m $* n"}],
   32.21 -    proc = K LeCancelNumerals.proc, identifier = []}];
   32.22 +    proc = K LeCancelNumerals.proc}];
   32.23  
   32.24  
   32.25  (*version without the hyps argument*)
   32.26 @@ -269,7 +269,7 @@
   32.27  val combine_numerals =
   32.28    Simplifier.make_simproc @{context} "int_combine_numerals"
   32.29      {lhss = [@{term "i $+ j"}, @{term "i $- j"}],
   32.30 -     proc = K CombineNumerals.proc, identifier = []};
   32.31 +     proc = K CombineNumerals.proc};
   32.32  
   32.33  
   32.34  
   32.35 @@ -315,7 +315,7 @@
   32.36  
   32.37  val combine_numerals_prod =
   32.38    Simplifier.make_simproc @{context} "int_combine_numerals_prod"
   32.39 -   {lhss = [@{term "i $* j"}], proc = K CombineNumeralsProd.proc, identifier = []};
   32.40 +   {lhss = [@{term "i $* j"}], proc = K CombineNumeralsProd.proc};
   32.41  
   32.42  end;
   32.43