removed obsolete Pure/General/history.ML;

--- a/src/Pure/General/ROOT.ML	Mon Jul 14 19:57:13 2008 +0200
+++ b/src/Pure/General/ROOT.ML	Mon Jul 14 19:57:14 2008 +0200
@@ -30,7 +30,6 @@
 use "url.ML";
 use "file.ML";
 use "buffer.ML";
-use "history.ML";
 use "xml.ML";
 use "yxml.ML";
 

--- a/src/Pure/General/history.ML	Mon Jul 14 19:57:13 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(*  Title:      Pure/General/history.ML
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Histories of values, with undo and redo, and optional limit.
-*)
-
-signature HISTORY =
-sig
-  type 'a T
-  val init: int option -> 'a -> 'a T
-  val is_initial: 'a T -> bool
-  val current: 'a T -> 'a
-  val previous: 'a T -> 'a option
-  val clear: int -> 'a T -> 'a T
-  val undo: 'a T -> 'a T
-  val redo: 'a T -> 'a T
-  val apply': 'a -> ('a -> 'a) -> 'a T -> 'a T
-  val apply: ('a -> 'a) -> 'a T -> 'a T
-  val map_current: ('a -> 'a) -> 'a T -> 'a T
-end;
-
-structure History: HISTORY =
-struct
-
-datatype 'a T =
-  History of 'a * (int option * int * 'a list * 'a list);
-
-fun init lim x = History (x, (lim, 0, [], []));
-
-fun is_initial (History (_, (_, len, _, _))) = len = 0;
-
-fun current (History (x, _)) = x;
-
-fun previous (History (_, (_, _, x :: _, _))) = SOME x
-  | previous _ = NONE;
-
-fun clear n (History (x, (lim, len, undo_list, redo_list))) =
-  History (x, (lim, Int.max (0, len - n), Library.drop (n, undo_list), redo_list));
-
-fun undo (History (_, (_, _, [], _))) = error "No further undo information"
-  | undo (History (x, (lim, len, u :: undo_list, redo_list))) =
-      History (u, (lim, len - 1, undo_list, x :: redo_list));
-
-fun redo (History (_, (_, _, _, []))) = error "No further redo information"
-  | redo (History (x, (lim, len, undo_list, r :: redo_list))) =
-      History (r, (lim, len + 1, x :: undo_list, redo_list));
-
-fun push NONE _ x xs = x :: xs
-  | push (SOME 0) _ _ _ = []
-  | push (SOME n) len x xs = if len < n then x :: xs else Library.take (n, x :: xs);
-
-fun apply' x' f (History (x, (lim, len, undo_list, _))) =
-  History (f x, (lim, len + 1, push lim len x' undo_list, []));
-
-fun apply f hist = apply' (current hist) f hist;
-
-fun map_current f (History (x, hist)) = History (f x, hist);
-
-end;

--- a/src/Pure/IsaMakefile	Mon Jul 14 19:57:13 2008 +0200
+++ b/src/Pure/IsaMakefile	Mon Jul 14 19:57:14 2008 +0200
@@ -25,15 +25,15 @@
 
 $(OUT)/Pure: General/ROOT.ML General/alist.ML General/balanced_tree.ML	\
   General/basics.ML General/buffer.ML General/file.ML General/graph.ML	\
-  General/heap.ML General/history.ML General/integer.ML			\
-  General/markup.ML General/name_space.ML General/ord_list.ML		\
-  General/output.ML General/path.ML General/position.ML			\
-  General/pretty.ML General/print_mode.ML General/scan.ML		\
-  General/secure.ML General/seq.ML General/source.ML General/stack.ML	\
-  General/susp.ML General/symbol.ML General/table.ML General/url.ML	\
-  General/xml.ML General/yxml.ML Isar/ROOT.ML Isar/antiquote.ML		\
-  Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML	\
-  Isar/class.ML Isar/code.ML Isar/code_unit.ML Isar/constdefs.ML	\
+  General/heap.ML General/integer.ML General/markup.ML			\
+  General/name_space.ML General/ord_list.ML General/output.ML		\
+  General/path.ML General/position.ML General/pretty.ML			\
+  General/print_mode.ML General/scan.ML General/secure.ML		\
+  General/seq.ML General/source.ML General/stack.ML General/susp.ML	\
+  General/symbol.ML General/table.ML General/url.ML General/xml.ML	\
+  General/yxml.ML Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML		\
+  Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML	\
+  Isar/code.ML Isar/code_unit.ML Isar/constdefs.ML			\
   Isar/context_rules.ML Isar/element.ML Isar/find_theorems.ML		\
   Isar/instance.ML Isar/isar.ML Isar/isar_cmd.ML Isar/isar_syn.ML	\
   Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML		\