# HG changeset patch
# User berghofe
# Date 1059061676 -7200
# Node ID d4e2ab7cc86bd15b8593ffc5b3c0890d2cdaf91f
# Parent  fd6d20c2371c3dd03a7eb02e7d0289a3f8469aa9
Exported function get_mode.

diff -r fd6d20c2371c -r d4e2ab7cc86b src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Jul 24 16:41:40 2003 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Jul 24 17:47:56 2003 +0200
@@ -17,6 +17,7 @@
   include BASIC_PROOF
   type context
   type state
+  datatype mode = Forward | ForwardChain | Backward
   exception STATE of string * state
   val check_result: string -> state -> 'a Seq.seq -> 'a Seq.seq
   val init_state: theory -> state
@@ -32,6 +33,7 @@
   val goal_facts: (state -> thm list) -> state -> state
   val use_facts: state -> state
   val reset_facts: state -> state
+  val get_mode: state -> mode
   val is_chain: state -> bool
   val assert_forward: state -> state
   val assert_forward_or_chain: state -> state