src/Pure/Isar/proof_node.ML

--- a/src/Pure/Isar/proof_node.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/Isar/proof_node.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -41,7 +41,7 @@
 
 (* apply transformer *)
 
-fun applys f (ProofNode (node as (st, _), n)) =
+fun applys f (ProofNode ((st, _), n)) =
   (case Seq.pull (f st) of
     NONE => error "empty result sequence -- proof command failed"
   | SOME res => ProofNode (res, n + 1));