# HG changeset patch
# User wenzelm
# Date 1414486632 -3600
# Node ID 6d71f19a9fd69e3dfbf2cde819da24ceac1fd664
# Parent  cc5a9a54d340b91bb782a8095991ac474e818081
more abstract type;

diff -r cc5a9a54d340 -r 6d71f19a9fd6 src/Pure/General/stack.ML
--- a/src/Pure/General/stack.ML	Tue Oct 28 09:32:18 2014 +0100
+++ b/src/Pure/General/stack.ML	Tue Oct 28 09:57:12 2014 +0100
@@ -6,7 +6,9 @@
 
 signature STACK =
 sig
-  type 'a T = 'a * 'a list
+  type 'a T
+  val make: 'a -> 'a list -> 'a T
+  val dest: 'a T -> 'a * 'a list
   val level: 'a T -> int
   val init: 'a -> 'a T
   val top: 'a T -> 'a
@@ -19,21 +21,27 @@
 structure Stack: STACK =
 struct
 
-type 'a T = 'a * 'a list;
-
-fun level (_, xs) = length xs;
+abstype 'a T = Stack of 'a * 'a list
+with
 
-fun init x = (x, []);
+fun make x xs = Stack (x, xs);
+fun dest (Stack (x, xs)) = (x, xs);
 
-fun top (x, _) = x;
+fun level (Stack (_, xs)) = length xs;
+
+fun init x = Stack (x, []);
 
-fun map_top f (x, xs) = (f x, xs);
+fun top (Stack (x, _)) = x;
 
-fun map_all f (x, xs) = (f x, map f xs);
+fun map_top f (Stack (x, xs)) = Stack (f x, xs);
 
-fun push (x, xs) = (x, x :: xs);
+fun map_all f (Stack (x, xs)) = Stack (f x, map f xs);
 
-fun pop (_, x :: xs) = (x, xs)
-  | pop (_, []) = raise List.Empty;
+fun push (Stack (x, xs)) = Stack (x, x :: xs);
+
+fun pop (Stack (_, x :: xs)) = Stack (x, xs)
+  | pop (Stack (_, [])) = raise List.Empty;
 
 end;
+
+end;
diff -r cc5a9a54d340 -r 6d71f19a9fd6 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Oct 28 09:32:18 2014 +0100
+++ b/src/Pure/Isar/proof.ML	Tue Oct 28 09:57:12 2014 +0100
@@ -302,18 +302,22 @@
 
 (* nested goal *)
 
-fun map_goal f g h (State (Node {context, facts, mode, goal = SOME goal}, node :: nodes)) =
+fun map_goal f g h (State stack) =
+  (case Stack.dest stack of
+    (Node {context, facts, mode, goal = SOME goal}, node :: nodes) =>
       let
         val Goal {statement, messages, using, goal, before_qed, after_qed} = goal;
         val goal' = make_goal (g (statement, messages, using, goal, before_qed, after_qed));
         val node' = map_node_context h node;
-      in State (make_node (f context, facts, mode, SOME goal'), node' :: nodes) end
-  | map_goal f g h (State (nd, node :: nodes)) =
+        val stack' = Stack.make (make_node (f context, facts, mode, SOME goal')) (node' :: nodes);
+      in State stack' end
+  | (nd, node :: nodes) =>
       let
         val nd' = map_node_context f nd;
-        val State (node', nodes') = map_goal f g h (State (node, nodes));
-      in State (nd', node' :: nodes') end
-  | map_goal _ _ _ state = state;
+        val State stack' = map_goal f g h (State (Stack.make node nodes));
+        val (node', nodes') = Stack.dest stack';
+      in State (Stack.make nd' (node' :: nodes')) end
+  | _ => State stack);
 
 fun provide_goal goal = map_goal I (fn (statement, _, using, _, before_qed, after_qed) =>
   (statement, [], using, goal, before_qed, after_qed)) I;