src/HOL/Statespace/state_space.ML
changeset 26496 49ae9456eba9
parent 26478 9d1029ce0e13
child 27276 ea82bd1e3c20
     1.1 --- a/src/HOL/Statespace/state_space.ML	Sat Mar 29 19:24:57 2008 +0100
     1.2 +++ b/src/HOL/Statespace/state_space.ML	Sat Mar 29 22:55:49 2008 +0100
     1.3 @@ -46,9 +46,6 @@
     1.4      val distinct_simproc : MetaSimplifier.simproc
     1.5  
     1.6  
     1.7 -    val change_simpset : (MetaSimplifier.simpset -> MetaSimplifier.simpset) ->
     1.8 -       Context.generic -> Context.generic
     1.9 -
    1.10      val get_comp : Context.generic -> string -> (Term.typ * string) Option.option
    1.11      val get_silent : Context.generic -> bool
    1.12      val set_silent : bool -> Context.generic -> Context.generic
    1.13 @@ -247,11 +244,6 @@
    1.14          | NONE => NONE)
    1.15        | _ => NONE))
    1.16  
    1.17 -fun change_simpset f =
    1.18 -     Context.mapping
    1.19 -       (fn thy  => (change_simpset_of thy f; thy))
    1.20 -       (fn ctxt => Simplifier.put_local_simpset (f (Simplifier.get_local_simpset ctxt)) ctxt);
    1.21 -
    1.22  fun read_typ thy s =
    1.23    Sign.read_typ thy s;
    1.24  
    1.25 @@ -309,7 +301,7 @@
    1.26            val tt' = tt |> fold upd all_names;
    1.27            val activate_simproc =
    1.28                Output.no_warnings
    1.29 -               (change_simpset (fn ss => ss addsimprocs [distinct_simproc]));
    1.30 +               (Simplifier.map_ss (fn ss => ss addsimprocs [distinct_simproc]));
    1.31            val ctxt' =
    1.32                ctxt
    1.33                |> NameSpaceData.put {declinfo=declinfo,distinctthm=tt',silent=silent}