src/Pure/ML/ml_antiquote.ML
changeset 47815 43f677b3ae91
parent 46987 15ce93dfe6da
child 48646 91281e9472d8
     1.1 --- a/src/Pure/ML/ml_antiquote.ML	Fri Apr 27 21:47:47 2012 +0200
     1.2 +++ b/src/Pure/ML/ml_antiquote.ML	Fri Apr 27 22:47:30 2012 +0200
     1.3 @@ -88,8 +88,7 @@
     1.4    macro (Binding.name "note")
     1.5      (Args.context :|-- (fn ctxt =>
     1.6        Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms
     1.7 -        >> (fn ((a, srcs), ths) =>
     1.8 -          ((a, map (Attrib.attribute (Proof_Context.theory_of ctxt)) srcs), [(ths, [])])))
     1.9 +        >> (fn ((a, srcs), ths) => ((a, map (Attrib.attribute_cmd ctxt) srcs), [(ths, [])])))
    1.10        >> (fn args => #2 (Proof_Context.note_thmss "" args ctxt)))) #>
    1.11  
    1.12    value (Binding.name "ctyp") (Args.typ >> (fn T =>