--- a/src/Pure/ML/ml_antiquotations.ML Mon Dec 08 16:04:50 2014 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML Mon Dec 08 22:42:12 2014 +0100
@@ -20,7 +20,7 @@
(fn src => fn output => fn ctxt =>
let
val (_, pos) = Token.name_of_src src;
- val (a, ctxt') = ML_Antiquotation.variant "output" ctxt;
+ val (a, ctxt') = ML_Context.variant "output" ctxt;
val env =
"val " ^ a ^ ": string -> unit =\n\
\ (" ^ output ^ ") o (fn s => s ^ Position.here (" ^
@@ -30,16 +30,6 @@
in (K (env, body), ctxt') end));
-(* embedded source *)
-
-val _ = Theory.setup
- (ML_Antiquotation.value @{binding source}
- (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 *)
val _ = Theory.setup