--- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Sat Mar 31 19:09:59 2012 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Sat Mar 31 19:26:23 2012 +0200
@@ -967,7 +967,7 @@
done
-declaration {* fn _ => Simplifier.map_ss (Simplifier.set_mksym (K (SOME o symmetric_fun))) *}
+declaration {* fn _ => Simplifier.map_ss (Simplifier.set_mksym Simplifier.default_mk_sym) *}
end
--- a/src/Pure/drule.ML Sat Mar 31 19:09:59 2012 +0200
+++ b/src/Pure/drule.ML Sat Mar 31 19:26:23 2012 +0200
@@ -43,7 +43,6 @@
val reflexive_thm: thm
val symmetric_thm: thm
val transitive_thm: thm
- val symmetric_fun: thm -> thm
val extensional: thm -> thm
val asm_rl: thm
val cut_rl: thm
@@ -400,8 +399,6 @@
val thm = Thm.implies_intr yz (Thm.transitive xythm yzthm);
in store_standard_thm_open (Binding.name "transitive") thm end;
-fun symmetric_fun thm = thm RS symmetric_thm;
-
fun extensional eq =
let val eq' =
Thm.abstract_rule "x" (Thm.dest_arg (fst (Thm.dest_equals (cprop_of eq)))) eq
--- a/src/Pure/raw_simplifier.ML Sat Mar 31 19:09:59 2012 +0200
+++ b/src/Pure/raw_simplifier.ML Sat Mar 31 19:26:23 2012 +0200
@@ -101,6 +101,7 @@
val solver: simpset -> solver -> int -> tactic
val simp_depth_limit_raw: Config.raw
val clear_ss: simpset -> simpset
+ val default_mk_sym: simpset -> thm -> thm option
val simproc_global_i: theory -> string -> term list
-> (theory -> simpset -> term -> thm option) -> simproc
val simproc_global: theory -> string -> string list
@@ -766,11 +767,13 @@
init_ss mk_rews termless subgoal_tac solvers
|> inherit_context ss;
+fun default_mk_sym _ th = SOME (th RS Drule.symmetric_thm);
+
val empty_ss =
init_ss
{mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
mk_cong = K I,
- mk_sym = K (SOME o Drule.symmetric_fun),
+ mk_sym = default_mk_sym,
mk_eq_True = K (K NONE),
reorient = default_reorient}
Term_Ord.termless (K (K no_tac)) ([], []);
--- a/src/Pure/simplifier.ML Sat Mar 31 19:09:59 2012 +0200
+++ b/src/Pure/simplifier.ML Sat Mar 31 19:26:23 2012 +0200
@@ -33,6 +33,7 @@
val map_simpset_global: (simpset -> simpset) -> theory -> theory
val pretty_ss: Proof.context -> simpset -> Pretty.T
val clear_ss: simpset -> simpset
+ val default_mk_sym: simpset -> thm -> thm option
val debug_bounds: bool Unsynchronized.ref
val prems_of: simpset -> thm list
val add_simp: thm -> simpset -> simpset