src/Pure/meta_simplifier.ML
changeset 14242 ec70653a02bf
parent 14040 8a2c8f762837
child 14330 eb8b8241ef5b
     1.1 --- a/src/Pure/meta_simplifier.ML	Fri Oct 17 11:04:36 2003 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Tue Oct 21 11:09:23 2003 +0200
     1.3 @@ -40,6 +40,9 @@
     1.4    val set_mk_rews       : meta_simpset * (thm -> thm list) -> meta_simpset
     1.5    val set_mk_sym        : meta_simpset * (thm -> thm option) -> meta_simpset
     1.6    val set_mk_eq_True    : meta_simpset * (thm -> thm option) -> meta_simpset
     1.7 +  val get_mk_rews       : meta_simpset -> thm -> thm list
     1.8 +  val get_mk_sym        : meta_simpset -> thm -> thm option
     1.9 +  val get_mk_eq_True    : meta_simpset -> thm -> thm option
    1.10    val set_termless      : meta_simpset * (term * term -> bool) -> meta_simpset
    1.11    val beta_eta_conversion: cterm -> thm
    1.12    val rewrite_cterm: bool * bool * bool ->
    1.13 @@ -518,6 +521,10 @@
    1.14              {mk= #mk mk_rews, mk_sym= #mk_sym mk_rews, mk_eq_True= mk_eq_True},
    1.15              termless,depth);
    1.16  
    1.17 +fun get_mk_rews    (Mss {mk_rews,...}) = #mk         mk_rews
    1.18 +fun get_mk_sym     (Mss {mk_rews,...}) = #mk_sym     mk_rews
    1.19 +fun get_mk_eq_True (Mss {mk_rews,...}) = #mk_eq_True mk_rews
    1.20 +
    1.21  (* termless *)
    1.22  
    1.23  fun set_termless