src/Pure/General/stack.ML

export just one setup function;
more antiquotations;
to_nnf: import open, avoiding internal variables (bounds);
ThmCache: added table of seen fact names;
reorganized skolem_thm/skolem_fact/saturate_skolem_cache: maintain seen fact names, ensure idempotent operation for Theory.at_end;
removed obsolete skolem attribute (NB: official fact name unavailable here);

(*  Title:      Pure/General/stack.ML
    ID:         $Id$
    Author:     Makarius

Non-empty stacks.
*)

signature STACK =
sig
  type 'a T (*= 'a * 'a list*)
  val level: 'a T -> int
  val init: 'a -> 'a T
  val top: 'a T -> 'a
  val map_top: ('a -> 'a) -> 'a T -> 'a T
  val map_all: ('a -> 'a) -> 'a T -> 'a T
  val push: 'a T -> 'a T
  val pop: 'a T -> 'a T      (*exception Empty*)
end;

structure Stack: STACK =
struct

type 'a T = 'a * 'a list;

fun level (_, xs) = length xs;

fun init x = (x, []);

fun top (x, _) = x;

fun map_top f (x, xs) = (f x, xs);

fun map_all f (x, xs) = (f x, map f xs);

fun push (x, xs) = (x, x :: xs);

fun pop (_, x :: xs) = (x, xs)
  | pop (_, []) = raise Empty;

end;