# HG changeset patch
# User wenzelm
# Date 928518911 -7200
# Node ID 55f1e6b639a46c55516c3a12a17c53ba171a7dee
# Parent  9d96ce9c27d6a59aacdccf788a84679d2d25df0d
added the_fact, level;

diff -r 9d96ce9c27d6 -r 55f1e6b639a4 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Jun 04 19:54:54 1999 +0200
+++ b/src/Pure/Isar/proof.ML	Fri Jun 04 19:55:11 1999 +0200
@@ -14,6 +14,7 @@
   val theory_of: state -> theory
   val sign_of: state -> Sign.sg
   val the_facts: state -> thm list
+  val the_fact: state -> thm
   val goal_facts: (state -> thm list) -> state -> state
   val use_facts: state -> state
   val reset_facts: state -> state
@@ -21,6 +22,7 @@
   val enter_forward: state -> state
   val verbose: bool ref
   val print_state: state -> unit
+  val level: state -> int
   type method
   val method: (thm list -> thm ->
     (thm * (indexname * term) list * (string * thm list) list) Seq.seq) -> method
@@ -179,6 +181,11 @@
 fun the_facts (State ({facts = Some facts, ...}, _)) = facts
   | the_facts state = raise STATE ("No current facts available", state);
 
+fun the_fact state =
+  (case the_facts state of
+    [fact] => fact
+  | _ => raise STATE ("Single fact expected", state));
+
 fun put_facts facts state =
   state
   |> map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal))
@@ -244,6 +251,8 @@
 
 (* blocks *)
 
+fun level (State (_, nodes)) = length nodes;
+
 fun open_block (State (node, nodes)) = State (node, node :: nodes);
 
 fun new_block state =