# HG changeset patch
# User wenzelm
# Date 1281543067 -7200
# Node ID f6c1e169f51b36c1aded9594834ba7fb90acab2a
# Parent  fd53ae1d4c4746a9545f4889dd9755323caa0223
removed obsolete Toplevel.enter_proof_body;

diff -r fd53ae1d4c47 -r f6c1e169f51b src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Aug 11 18:10:39 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Aug 11 18:11:07 2010 +0200
@@ -20,7 +20,6 @@
   val theory_of: state -> theory
   val proof_of: state -> Proof.state
   val proof_position_of: state -> int
-  val enter_proof_body: state -> Proof.state
   val end_theory: Position.T -> state -> theory
   val print_state_context: state -> unit
   val print_state: bool -> state -> unit
@@ -186,8 +185,6 @@
     Proof (prf, _) => Proof_Node.position prf
   | _ => raise UNDEF);
 
-val enter_proof_body = node_case (Proof.init o Context.proof_of) Proof.enter_forward;
-
 fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = Theory.end_theory thy
   | end_theory pos _ = error ("Unfinished theory at end of input" ^ Position.str_of pos);