src/Pure/raw_simplifier.ML
changeset 62913 13252110a6fe
parent 62876 507c90523113
child 63221 7d43fbbaba28
     1.1 --- a/src/Pure/raw_simplifier.ML	Thu Apr 07 22:09:23 2016 +0200
     1.2 +++ b/src/Pure/raw_simplifier.ML	Fri Apr 08 20:15:20 2016 +0200
     1.3 @@ -36,8 +36,7 @@
     1.4    type simproc
     1.5    val eq_simproc: simproc * simproc -> bool
     1.6    val cert_simproc: theory -> string ->
     1.7 -    {lhss: term list, proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list}
     1.8 -    -> simproc
     1.9 +    {lhss: term list, proc: morphism -> Proof.context -> cterm -> thm option} -> simproc
    1.10    val transform_simproc: morphism -> simproc -> simproc
    1.11    val simpset_of: Proof.context -> simpset
    1.12    val put_simpset: simpset -> Proof.context -> Proof.context
    1.13 @@ -220,12 +219,9 @@
    1.14     {name: string,
    1.15      lhs: term,
    1.16      proc: Proof.context -> cterm -> thm option,
    1.17 -    id: stamp * thm list};
    1.18 +    stamp: stamp};
    1.19  
    1.20 -fun eq_procid ((s1: stamp, ths1: thm list), (s2, ths2)) =
    1.21 -  s1 = s2 andalso eq_list Thm.eq_thm (ths1, ths2);
    1.22 -
    1.23 -fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = eq_procid (id1, id2);
    1.24 +fun eq_proc (Proc {stamp = stamp1, ...}, Proc {stamp = stamp2, ...}) = stamp1 = stamp2;
    1.25  
    1.26  
    1.27  (* solvers *)
    1.28 @@ -298,8 +294,8 @@
    1.29   {simps = Net.entries rules
    1.30      |> map (fn {name, thm, ...} => (name, thm)),
    1.31    procs = Net.entries procs
    1.32 -    |> map (fn Proc {name, lhs, id, ...} => ((name, lhs), id))
    1.33 -    |> partition_eq (eq_snd eq_procid)
    1.34 +    |> map (fn Proc {name, lhs, stamp, ...} => ((name, lhs), stamp))
    1.35 +    |> partition_eq (eq_snd op =)
    1.36      |> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)),
    1.37    congs = #1 congs,
    1.38    weak_congs = #2 congs,
    1.39 @@ -667,20 +663,19 @@
    1.40      {name: string,
    1.41       lhss: term list,
    1.42       proc: morphism -> Proof.context -> cterm -> thm option,
    1.43 -     id: stamp * thm list};
    1.44 +     stamp: stamp};
    1.45  
    1.46 -fun eq_simproc (Simproc {id = id1, ...}, Simproc {id = id2, ...}) = eq_procid (id1, id2);
    1.47 +fun eq_simproc (Simproc {stamp = stamp1, ...}, Simproc {stamp = stamp2, ...}) = stamp1 = stamp2;
    1.48  
    1.49 -fun cert_simproc thy name {lhss, proc, identifier} =
    1.50 -  Simproc {name = name, lhss = map (Sign.cert_term thy) lhss, proc = proc,
    1.51 -    id = (stamp (), map Thm.trim_context identifier)};
    1.52 +fun cert_simproc thy name {lhss, proc} =
    1.53 +  Simproc {name = name, lhss = map (Sign.cert_term thy) lhss, proc = proc, stamp = stamp ()};
    1.54  
    1.55 -fun transform_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) =
    1.56 +fun transform_simproc phi (Simproc {name, lhss, proc, stamp}) =
    1.57    Simproc
    1.58     {name = name,
    1.59      lhss = map (Morphism.term phi) lhss,
    1.60      proc = Morphism.transform phi proc,
    1.61 -    id = (s, Morphism.fact phi ths)};
    1.62 +    stamp = stamp};
    1.63  
    1.64  local
    1.65  
    1.66 @@ -704,8 +699,8 @@
    1.67      (cond_warning ctxt (fn () => "Simplification procedure " ^ quote name ^ " not in simpset");
    1.68        ctxt);
    1.69  
    1.70 -fun prep_procs (Simproc {name, lhss, proc, id}) =
    1.71 -  lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, id = id});
    1.72 +fun prep_procs (Simproc {name, lhss, proc, stamp}) =
    1.73 +  lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, stamp = stamp});
    1.74  
    1.75  in
    1.76