--- a/src/Pure/ML/ml_antiquotations.ML Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML Sun Nov 30 12:24:56 2014 +0100
@@ -34,10 +34,10 @@
val _ = Theory.setup
(ML_Antiquotation.value @{binding source}
- (Scan.lift Args.text_source_position >> (fn {delimited, text, range} =>
- "{delimited = " ^ Bool.toString delimited ^
- ", text = " ^ ML_Syntax.print_string text ^
- ", range = " ^ ML_Syntax.print_range range ^ "}")));
+ (Scan.lift Args.text_source_position >> (fn source =>
+ "Input.source " ^ Bool.toString (Input.is_delimited source) ^ " " ^
+ ML_Syntax.print_string (Input.text_of source) ^ " " ^
+ ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))));
(* formal entities *)