src/Pure/ML/ml_context.ML
changeset 55743 225a060e7445
parent 55526 39708e59f4b0
child 55828 42ac3cfb89f6
     1.1 --- a/src/Pure/ML/ml_context.ML	Tue Feb 25 14:34:18 2014 +0100
     1.2 +++ b/src/Pure/ML/ml_context.ML	Tue Feb 25 14:56:58 2014 +0100
     1.3 @@ -25,7 +25,7 @@
     1.4    val ml_store_thm: string * thm -> unit
     1.5    type antiq = Proof.context -> string * string
     1.6    val add_antiq: binding -> antiq context_parser -> theory -> theory
     1.7 -  val check_antiq: theory -> xstring * Position.T -> string
     1.8 +  val check_antiq: Proof.context -> xstring * Position.T -> string
     1.9    val trace_raw: Config.raw
    1.10    val trace: bool Config.T
    1.11    val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
    1.12 @@ -107,16 +107,17 @@
    1.13    fun merge data : T = Name_Space.merge_tables data;
    1.14  );
    1.15  
    1.16 +val get_antiqs = Antiq_Parsers.get o Proof_Context.theory_of;
    1.17 +
    1.18  fun add_antiq name scan thy = thy
    1.19    |> Antiq_Parsers.map (Name_Space.define (Context.Theory thy) true (name, scan) #> snd);
    1.20  
    1.21 -fun check_antiq thy = #1 o Name_Space.check (Context.Theory thy) (Antiq_Parsers.get thy);
    1.22 +fun check_antiq ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_antiqs ctxt);
    1.23  
    1.24  fun antiquotation src ctxt =
    1.25    let
    1.26 -    val thy = Proof_Context.theory_of ctxt;
    1.27      val ((xname, _), pos) = Args.dest_src src;
    1.28 -    val (_, scan) = Name_Space.check (Context.Proof ctxt) (Antiq_Parsers.get thy) (xname, pos);
    1.29 +    val (_, scan) = Name_Space.check (Context.Proof ctxt) (get_antiqs ctxt) (xname, pos);
    1.30    in Args.context_syntax Markup.ML_antiquotationN scan src ctxt end;
    1.31  
    1.32