# HG changeset patch
# User wenzelm
# Date 1333214783 -7200
# Node ID 0b1829860149a48b9150035ca8f232961fff6443
# Parent  289dcbdd59849ba162bee9314a2a1044fd519bc8
tuned signature;

diff -r 289dcbdd5984 -r 0b1829860149 src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy
--- 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
diff -r 289dcbdd5984 -r 0b1829860149 src/Pure/drule.ML
--- 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
diff -r 289dcbdd5984 -r 0b1829860149 src/Pure/raw_simplifier.ML
--- 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)) ([], []);
diff -r 289dcbdd5984 -r 0b1829860149 src/Pure/simplifier.ML
--- 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