1.1 --- a/src/Pure/simplifier.ML	Sun Feb 04 22:02:15 2007 +0100
     1.2 +++ b/src/Pure/simplifier.ML	Sun Feb 04 22:02:16 2007 +0100
     1.3 @@ -70,9 +70,11 @@
     1.4    val cong_add: attribute
     1.5    val cong_del: attribute
     1.6    val get_simproc: Proof.context -> xstring -> simproc
     1.7 -  val def_simproc: string -> string list -> (morphism -> simpset -> cterm -> thm option) ->
     1.8 +  val def_simproc: {name: string, lhss: string list,
     1.9 +    proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} ->
    1.10      local_theory -> local_theory
    1.11 -  val def_simproc_i: string -> term list -> (morphism -> simpset -> cterm -> thm option) ->
    1.12 +  val def_simproc_i: {name: string, lhss: term list,
    1.13 +    proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} ->
    1.14      local_theory -> local_theory
    1.15    val cong_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    1.16    val simp_modifiers': (Args.T list -> (Method.modifier * Args.T list)) list
    1.17 @@ -172,15 +174,16 @@
    1.18  fun err_dup_simprocs ds =
    1.19    error ("Duplicate simproc(s): " ^ commas_quote ds);
    1.20  
    1.21 +
    1.22  (* data *)
    1.23  
    1.24  structure Simprocs = GenericDataFun
    1.25  (
    1.26    val name = "Pure/simprocs";
    1.27 -  type T = (simproc * stamp) NameSpace.table;
    1.28 +  type T = simproc NameSpace.table;
    1.29    val empty = NameSpace.empty_table;
    1.30    val extend = I;
    1.31 -  fun merge _ simprocs = NameSpace.merge_tables (eq_snd (op =)) simprocs
    1.32 +  fun merge _ simprocs = NameSpace.merge_tables eq_simproc simprocs
    1.33      handle Symtab.DUPS ds => err_dup_simprocs ds;
    1.34    fun print _ _ = ();
    1.35  );
    1.36 @@ -195,7 +198,7 @@
    1.37      val name = NameSpace.intern space xname;
    1.38    in
    1.39      (case Symtab.lookup tab name of
    1.40 -      SOME (proc, _) => proc
    1.41 +      SOME proc => proc
    1.42      | NONE => error ("Undefined simplification procedure: " ^ quote name))
    1.43    end;
    1.44  
    1.45 @@ -216,34 +219,33 @@
    1.46  (* FIXME *)
    1.47  fun cert_terms ctxt ts = map (ProofContext.cert_term ctxt) ts;
    1.48  
    1.49 -fun prep_pats prep ctxt raw_pats =
    1.50 +fun gen_simproc prep {name, lhss, proc, identifier} lthy =
    1.51    let
    1.52 -    val pats = prep ctxt raw_pats;
    1.53 -    val ctxt' = ctxt
    1.54 -      |> fold Variable.declare_term pats
    1.55 -      |> fold Variable.auto_fixes pats;
    1.56 -  in Variable.export_terms ctxt' ctxt pats end;
    1.57 -
    1.58 -fun gen_simproc prep name raw_pats proc lthy =
    1.59 -  let
    1.60 -    val pats =
    1.61 -      prep_pats prep lthy raw_pats
    1.62 -      |> map (Morphism.term (LocalTheory.target_morphism lthy));
    1.63 -    val naming = LocalTheory.target_naming lthy;
    1.64 +    val naming = LocalTheory.full_naming lthy;
    1.65 +    val simproc = make_simproc
    1.66 +      {name = LocalTheory.full_name lthy name,
    1.67 +       lhss =
    1.68 +        let
    1.69 +          val lhss' = prep lthy lhss;
    1.70 +          val ctxt' = lthy
    1.71 +            |> fold Variable.declare_term lhss'
    1.72 +            |> fold Variable.auto_fixes lhss';
    1.73 +        in Variable.export_terms ctxt' lthy lhss' end
    1.74 +        |> map (Thm.cterm_of (ProofContext.theory_of lthy)),
    1.75 +       proc = proc,
    1.76 +       identifier = identifier}
    1.77 +      |> morph_simproc (LocalTheory.target_morphism lthy);
    1.78    in
    1.79      lthy |> LocalTheory.declaration (fn phi => fn context =>
    1.80        let
    1.81 -        val cert = Thm.cterm_of (Context.theory_of context);
    1.82 -        val pats' = map (cert o Morphism.term phi) pats;
    1.83          val name' = Morphism.name phi name;
    1.84 -        val proc' = proc phi;
    1.85 -        val simproc = mk_simproc' (NameSpace.full naming name') pats' proc';
    1.86 +        val simproc' = morph_simproc phi simproc;
    1.87        in
    1.88          context
    1.89          |> Simprocs.map (fn simprocs =>
    1.90 -            NameSpace.extend_table naming (simprocs, [(name', (simproc, stamp ()))])
    1.91 +            NameSpace.extend_table naming (simprocs, [(name', simproc')])
    1.92                handle Symtab.DUPS ds => err_dup_simprocs ds)
    1.93 -        |> map_ss (fn ss => ss addsimprocs [simproc])
    1.94 +        |> map_ss (fn ss => ss addsimprocs [simproc'])
    1.95        end)
    1.96    end;
    1.97