# HG changeset patch # User wenzelm # Date 1453644149 -3600 # Node ID e099a94290c15cca8fe6bd4f066a37fd43ab226a # Parent 6ee95b93fbed51eb547a706104b5ecb37f2d570b tuned; diff -r 6ee95b93fbed -r e099a94290c1 src/Pure/ML/ml_antiquotations.ML --- a/src/Pure/ML/ml_antiquotations.ML Sun Jan 24 14:58:56 2016 +0100 +++ b/src/Pure/ML/ml_antiquotations.ML Sun Jan 24 15:02:29 2016 +0100 @@ -11,7 +11,7 @@ val _ = Theory.setup (ML_Antiquotation.value @{binding cartouche} - (Args.context -- Scan.lift (Parse.position Args.cartouche_input) >> (fn (ctxt, (source, pos)) => + (Scan.lift Args.cartouche_input >> (fn source => "Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^ ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))) #>