src/Pure/raw_simplifier.ML
changeset 47239 0b1829860149
parent 46707 1427dcc7c9a6
child 48992 0518bf89c777
     1.1 --- a/src/Pure/raw_simplifier.ML	Sat Mar 31 19:09:59 2012 +0200
     1.2 +++ b/src/Pure/raw_simplifier.ML	Sat Mar 31 19:26:23 2012 +0200
     1.3 @@ -101,6 +101,7 @@
     1.4    val solver: simpset -> solver -> int -> tactic
     1.5    val simp_depth_limit_raw: Config.raw
     1.6    val clear_ss: simpset -> simpset
     1.7 +  val default_mk_sym: simpset -> thm -> thm option
     1.8    val simproc_global_i: theory -> string -> term list
     1.9      -> (theory -> simpset -> term -> thm option) -> simproc
    1.10    val simproc_global: theory -> string -> string list
    1.11 @@ -766,11 +767,13 @@
    1.12    init_ss mk_rews termless subgoal_tac solvers
    1.13    |> inherit_context ss;
    1.14  
    1.15 +fun default_mk_sym _ th = SOME (th RS Drule.symmetric_thm);
    1.16 +
    1.17  val empty_ss =
    1.18    init_ss
    1.19      {mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
    1.20        mk_cong = K I,
    1.21 -      mk_sym = K (SOME o Drule.symmetric_fun),
    1.22 +      mk_sym = default_mk_sym,
    1.23        mk_eq_True = K (K NONE),
    1.24        reorient = default_reorient}
    1.25      Term_Ord.termless (K (K no_tac)) ([], []);