src/Pure/raw_simplifier.ML
changeset 61144 5e94dfead1c2
parent 61098 e1b4b24f2ebd
child 61354 1727d7d14d76
     1.1 --- a/src/Pure/raw_simplifier.ML	Wed Sep 09 14:47:41 2015 +0200
     1.2 +++ b/src/Pure/raw_simplifier.ML	Wed Sep 09 20:57:21 2015 +0200
     1.3 @@ -35,10 +35,10 @@
     1.4      safe_solvers: string list}
     1.5    type simproc
     1.6    val eq_simproc: simproc * simproc -> bool
     1.7 +  val cert_simproc: theory -> string ->
     1.8 +    {lhss: term list, proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list}
     1.9 +    -> simproc
    1.10    val transform_simproc: morphism -> simproc -> simproc
    1.11 -  val make_simproc: {name: string, lhss: cterm list,
    1.12 -    proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list} -> simproc
    1.13 -  val mk_simproc: string -> cterm list -> (Proof.context -> term -> thm option) -> simproc
    1.14    val simpset_of: Proof.context -> simpset
    1.15    val put_simpset: simpset -> Proof.context -> Proof.context
    1.16    val simpset_map: Proof.context -> (Proof.context -> Proof.context) -> simpset -> simpset
    1.17 @@ -105,10 +105,6 @@
    1.18    val solver: Proof.context -> solver -> int -> tactic
    1.19    val simp_depth_limit_raw: Config.raw
    1.20    val default_mk_sym: Proof.context -> thm -> thm option
    1.21 -  val simproc_global_i: theory -> string -> term list ->
    1.22 -    (Proof.context -> term -> thm option) -> simproc
    1.23 -  val simproc_global: theory -> string -> string list ->
    1.24 -    (Proof.context -> term -> thm option) -> simproc
    1.25    val simp_trace_depth_limit_raw: Config.raw
    1.26    val simp_trace_raw: Config.raw
    1.27    val simp_debug_raw: Config.raw
    1.28 @@ -675,6 +671,10 @@
    1.29  
    1.30  fun eq_simproc (Simproc {id = id1, ...}, Simproc {id = id2, ...}) = eq_procid (id1, id2);
    1.31  
    1.32 +fun cert_simproc thy name {lhss, proc, identifier} =
    1.33 +  Simproc {name = name, lhss = map (Sign.cert_term thy) lhss, proc = proc,
    1.34 +    id = (stamp (), map Thm.trim_context identifier)};
    1.35 +
    1.36  fun transform_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) =
    1.37    Simproc
    1.38     {name = name,
    1.39 @@ -682,19 +682,6 @@
    1.40      proc = Morphism.transform phi proc,
    1.41      id = (s, Morphism.fact phi ths)};
    1.42  
    1.43 -fun make_simproc {name, lhss, proc, identifier} =
    1.44 -  Simproc {name = name, lhss = map Thm.term_of lhss, proc = proc,
    1.45 -    id = (stamp (), map Thm.trim_context identifier)};
    1.46 -
    1.47 -fun mk_simproc name lhss proc =
    1.48 -  make_simproc {name = name, lhss = lhss, proc = fn _ => fn ctxt => fn ct =>
    1.49 -    proc ctxt (Thm.term_of ct), identifier = []};
    1.50 -
    1.51 -(* FIXME avoid global thy and Logic.varify_global *)
    1.52 -fun simproc_global_i thy name = mk_simproc name o map (Thm.global_cterm_of thy o Logic.varify_global);
    1.53 -fun simproc_global thy name = simproc_global_i thy name o map (Syntax.read_term_global thy);
    1.54 -
    1.55 -
    1.56  local
    1.57  
    1.58  fun add_proc (proc as Proc {name, lhs, ...}) ctxt =