src/Pure/raw_simplifier.ML
changeset 54895 515630483010
parent 54883 dd04a8b654fc
child 54982 b327bf0dabfb
     1.1 --- a/src/Pure/raw_simplifier.ML	Wed Jan 01 13:24:23 2014 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Wed Jan 01 14:29:22 2014 +0100
     1.3 @@ -40,7 +40,6 @@
     1.4    val mk_simproc: string -> cterm list -> (Proof.context -> term -> thm option) -> simproc
     1.5    val simpset_of: Proof.context -> simpset
     1.6    val put_simpset: simpset -> Proof.context -> Proof.context
     1.7 -  val global_context: theory -> simpset -> Proof.context
     1.8    val simpset_map: Proof.context -> (Proof.context -> Proof.context) -> simpset -> simpset
     1.9    val map_theory_simpset: (Proof.context -> Proof.context) -> theory -> theory
    1.10    val empty_simpset: Proof.context -> Proof.context
    1.11 @@ -388,8 +387,6 @@
    1.12      val Simpset ({bounds, depth, ...}, _) = context_ss;
    1.13    in Simpset (make_ss1 (rules, prems, bounds, depth), ss2) end);
    1.14  
    1.15 -fun global_context thy ss = Proof_Context.init_global thy |> put_simpset ss;
    1.16 -
    1.17  val empty_simpset = put_simpset empty_ss;
    1.18  
    1.19  fun map_theory_simpset f thy =