--- a/src/Pure/Thy/thy_output.ML Mon Sep 10 12:13:39 2012 +0200
+++ b/src/Pure/Thy/thy_output.ML Mon Sep 10 13:19:56 2012 +0200
@@ -42,6 +42,7 @@
val maybe_pretty_source: (Proof.context -> 'a -> Pretty.T) -> Proof.context ->
Args.src -> 'a list -> Pretty.T list
val output: Proof.context -> Pretty.T list -> string
+ val verb_text: string -> string
end;
structure Thy_Output: THY_OUTPUT =
@@ -685,14 +686,4 @@
end;
-
-(* files *)
-
-val _ =
- Context.>> (Context.map_theory
- (antiquotation (Binding.name "file") (Scan.lift Args.name)
- (fn _ => fn path =>
- if File.exists (Path.explode path) then verb_text path
- else error ("Bad file: " ^ quote path))));
-
end;