# HG changeset patch # User wenzelm # Date 1441229501 -7200 # Node ID e1b4b24f2ebd924870e1f9dc4aab8a2f94e83a24 # Parent 93f08a05abc95cc03cd801db5939e95e9669f0b0 eliminated pointless cterms; diff -r 93f08a05abc9 -r e1b4b24f2ebd src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Wed Sep 02 23:18:39 2015 +0200 +++ b/src/Pure/raw_simplifier.ML Wed Sep 02 23:31:41 2015 +0200 @@ -27,7 +27,7 @@ val merge_ss: simpset * simpset -> simpset val dest_ss: simpset -> {simps: (string * thm) list, - procs: (string * cterm list) list, + procs: (string * term list) list, congs: (cong_name * thm) list, weak_congs: cong_name list, loopers: string list, @@ -222,7 +222,7 @@ datatype proc = Proc of {name: string, - lhs: cterm, + lhs: term, proc: Proof.context -> cterm -> thm option, id: stamp * thm list}; @@ -669,7 +669,7 @@ datatype simproc = Simproc of {name: string, - lhss: cterm list, + lhss: term list, proc: morphism -> Proof.context -> cterm -> thm option, id: stamp * thm list}; @@ -678,12 +678,13 @@ fun transform_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) = Simproc {name = name, - lhss = map (Morphism.cterm phi) lhss, + lhss = map (Morphism.term phi) lhss, proc = Morphism.transform phi proc, id = (s, Morphism.fact phi ths)}; fun make_simproc {name, lhss, proc, identifier} = - Simproc {name = name, lhss = lhss, proc = proc, id = (stamp (), identifier)}; + Simproc {name = name, lhss = map Thm.term_of lhss, proc = proc, + id = (stamp (), map Thm.trim_context identifier)}; fun mk_simproc name lhss proc = make_simproc {name = name, lhss = lhss, proc = fn _ => fn ctxt => fn ct => @@ -698,10 +699,10 @@ fun add_proc (proc as Proc {name, lhs, ...}) ctxt = (cond_tracing ctxt (fn () => - print_term ctxt ("Adding simplification procedure " ^ quote name ^ " for") (Thm.term_of lhs)); + print_term ctxt ("Adding simplification procedure " ^ quote name ^ " for") lhs); ctxt |> map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => - (congs, Net.insert_term eq_proc (Thm.term_of lhs, proc) procs, + (congs, Net.insert_term eq_proc (lhs, proc) procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)) handle Net.INSERT => (cond_warning ctxt (fn () => "Ignoring duplicate simplification procedure " ^ quote name); @@ -710,7 +711,7 @@ fun del_proc (proc as Proc {name, lhs, ...}) ctxt = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => - (congs, Net.delete_term eq_proc (Thm.term_of lhs, proc) procs, + (congs, Net.delete_term eq_proc (lhs, proc) procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)) handle Net.DELETE => (cond_warning ctxt (fn () => "Simplification procedure " ^ quote name ^ " not in simpset"); @@ -1006,7 +1007,7 @@ fun proc_rews [] = NONE | proc_rews (Proc {name, proc, lhs, ...} :: ps) = - if Pattern.matches (Proof_Context.theory_of ctxt) (Thm.term_of lhs, Thm.term_of t) then + if Pattern.matches (Proof_Context.theory_of ctxt) (lhs, Thm.term_of t) then (cond_tracing' ctxt simp_debug (fn () => print_term ctxt ("Trying procedure " ^ quote name ^ " on:") eta_t); (case proc ctxt eta_t' of diff -r 93f08a05abc9 -r e1b4b24f2ebd src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Wed Sep 02 23:18:39 2015 +0200 +++ b/src/Pure/simplifier.ML Wed Sep 02 23:31:41 2015 +0200 @@ -167,7 +167,7 @@ fun pretty_simproc (name, lhss) = Pretty.block (Pretty.mark_str name :: Pretty.str ":" :: Pretty.fbrk :: - Pretty.fbreaks (map (Pretty.item o single o pretty_term o Thm.term_of) lhss)); + Pretty.fbreaks (map (Pretty.item o single o pretty_term) lhss)); fun pretty_cong_name (const, name) = pretty_term ((if const then Const else Free) (name, dummyT));