removed obsolete Toplevel.enter_proof_body;
authorwenzelm
Wed Aug 11 18:11:07 2010 +0200 (2010-08-11 ago)
changeset 38337f6c1e169f51b
parent 38336 fd53ae1d4c47
child 38351 ea1ee55aa41f
removed obsolete Toplevel.enter_proof_body;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Aug 11 18:10:39 2010 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Aug 11 18:11:07 2010 +0200
     1.3 @@ -20,7 +20,6 @@
     1.4    val theory_of: state -> theory
     1.5    val proof_of: state -> Proof.state
     1.6    val proof_position_of: state -> int
     1.7 -  val enter_proof_body: state -> Proof.state
     1.8    val end_theory: Position.T -> state -> theory
     1.9    val print_state_context: state -> unit
    1.10    val print_state: bool -> state -> unit
    1.11 @@ -186,8 +185,6 @@
    1.12      Proof (prf, _) => Proof_Node.position prf
    1.13    | _ => raise UNDEF);
    1.14  
    1.15 -val enter_proof_body = node_case (Proof.init o Context.proof_of) Proof.enter_forward;
    1.16 -
    1.17  fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = Theory.end_theory thy
    1.18    | end_theory pos _ = error ("Unfinished theory at end of input" ^ Position.str_of pos);
    1.19