moved 'latex' from library.ML to goals.ML;

--- a/src/Pure/goals.ML	Wed Nov 12 16:21:15 1997 +0100
+++ b/src/Pure/goals.ML	Wed Nov 12 16:21:26 1997 +0100
@@ -447,6 +447,12 @@
 
 fun pprint_typ T = Sign.pprint_typ (top_sg()) T;
 
+(* FIXME !? *)
+(* output to LaTeX / xdvi *)
+fun latex s =
+  execute ("( cd /tmp ; echo \"" ^ s ^
+    "\" | isa2latex -s > $$.tex ; latex $$.tex ; xdvi $$.dvi ; rm $$.* ) > /dev/null &");
+
 (* Redirect output of function f:unit->unit to LaTeX *)
 fun redirect_to_latex f =
 	let