src/Pure/Isar/proof.ML
changeset 6776 55f1e6b639a4
parent 6756 fe6eb161df3e
child 6790 0a39f22f847a
     1.1 --- a/src/Pure/Isar/proof.ML	Fri Jun 04 19:54:54 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Fri Jun 04 19:55:11 1999 +0200
     1.3 @@ -14,6 +14,7 @@
     1.4    val theory_of: state -> theory
     1.5    val sign_of: state -> Sign.sg
     1.6    val the_facts: state -> thm list
     1.7 +  val the_fact: state -> thm
     1.8    val goal_facts: (state -> thm list) -> state -> state
     1.9    val use_facts: state -> state
    1.10    val reset_facts: state -> state
    1.11 @@ -21,6 +22,7 @@
    1.12    val enter_forward: state -> state
    1.13    val verbose: bool ref
    1.14    val print_state: state -> unit
    1.15 +  val level: state -> int
    1.16    type method
    1.17    val method: (thm list -> thm ->
    1.18      (thm * (indexname * term) list * (string * thm list) list) Seq.seq) -> method
    1.19 @@ -179,6 +181,11 @@
    1.20  fun the_facts (State ({facts = Some facts, ...}, _)) = facts
    1.21    | the_facts state = raise STATE ("No current facts available", state);
    1.22  
    1.23 +fun the_fact state =
    1.24 +  (case the_facts state of
    1.25 +    [fact] => fact
    1.26 +  | _ => raise STATE ("Single fact expected", state));
    1.27 +
    1.28  fun put_facts facts state =
    1.29    state
    1.30    |> map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal))
    1.31 @@ -244,6 +251,8 @@
    1.32  
    1.33  (* blocks *)
    1.34  
    1.35 +fun level (State (_, nodes)) = length nodes;
    1.36 +
    1.37  fun open_block (State (node, nodes)) = State (node, node :: nodes);
    1.38  
    1.39  fun new_block state =