src/Pure/simplifier.ML
changeset 35232 f588e1169c8b
parent 33673 4b0f2599ed48
child 35613 9d3ff36ad4e1
     1.1 --- a/src/Pure/simplifier.ML	Fri Feb 19 11:56:11 2010 +0100
     1.2 +++ b/src/Pure/simplifier.ML	Fri Feb 19 16:11:45 2010 +0100
     1.3 @@ -36,7 +36,7 @@
     1.4    val inherit_context: simpset -> simpset -> simpset
     1.5    val the_context: simpset -> Proof.context
     1.6    val context: Proof.context -> simpset -> simpset
     1.7 -  val theory_context: theory  -> simpset -> simpset
     1.8 +  val global_context: theory  -> simpset -> simpset
     1.9    val simproc_i: theory -> string -> term list
    1.10      -> (theory -> simpset -> term -> thm option) -> simproc
    1.11    val simproc: theory -> string -> string list