# HG changeset patch
# User wenzelm
# Date 931288011 -7200
# Node ID 4125d6b6d8f9f4e3ba12e23b028d052bedefd857
# Parent  682f8a9ec75d40e5dfe60cc886c20fbd7a7578d1
removed proof history nesting commands (not useful);

diff -r 682f8a9ec75d -r 4125d6b6d8f9 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Jul 06 21:06:03 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jul 06 21:06:51 1999 +0200
@@ -396,18 +396,6 @@
   OuterSyntax.improper_command "back" "backtracking of proof command" K.prf_script
     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.back));
 
-val prevP =
-  OuterSyntax.improper_command "prev" "previous proof state" K.control
-    (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.prev));
-
-val upP =
-  OuterSyntax.improper_command "up" "upper proof state" K.control
-    (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.up));
-
-val topP =
-  OuterSyntax.improper_command "top" "to initial proof state" K.control
-    (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.top));
-
 
 (* history *)
 
@@ -565,7 +553,7 @@
   fixP, letP, thenP, fromP, withP, noteP, beginP, endP, nextP,
   qed_withP, qedP, terminal_proofP, immediate_proofP, default_proofP,
   skip_proofP, applyP, then_applyP, proofP, alsoP, finallyP, backP,
-  prevP, upP, topP, cannot_undoP, clear_undoP, redoP, undos_proofP,
+  cannot_undoP, clear_undoP, redoP, undos_proofP,
   kill_proofP, undoP,
   (*diagnostic commands*)
   print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
diff -r 682f8a9ec75d -r 4125d6b6d8f9 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Tue Jul 06 21:06:03 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Tue Jul 06 21:06:51 1999 +0200
@@ -271,35 +271,34 @@
 fun global_statement_i f (name, atts, t) int thy =
   ProofHistory.init (Toplevel.undo_limit int) (f name atts t thy);
 
-fun local_statement do_open f g (name, src, s) = ProofHistory.apply_cond_open do_open (fn state =>
+fun local_statement f g (name, src, s) = ProofHistory.apply (fn state =>
   f name (map (Attrib.local_attribute (Proof.theory_of state)) src) s (g state));
 
-fun local_statement_i do_open f g (name, atts, t) =
-  ProofHistory.apply_cond_open do_open (f name atts t o g);
+fun local_statement_i f g (name, atts, t) = ProofHistory.apply (f name atts t o g);
 
 val theorem   = global_statement Proof.theorem o Comment.ignore;
 val theorem_i = global_statement_i Proof.theorem_i o Comment.ignore;
 val lemma     = global_statement Proof.lemma o Comment.ignore;
 val lemma_i   = global_statement_i Proof.lemma_i o Comment.ignore;
-val assume    = local_statement false (Proof.assume assume_tac) I o Comment.ignore;
-val assume_i  = local_statement_i false (Proof.assume_i assume_tac) I o Comment.ignore;
-val presume   = local_statement false (Proof.assume (K all_tac)) I o Comment.ignore;
-val presume_i = local_statement_i false (Proof.assume_i (K all_tac)) I o Comment.ignore;
-val show      = local_statement true Proof.show I o Comment.ignore;
-val show_i    = local_statement_i true Proof.show_i I o Comment.ignore;
-val have      = local_statement true Proof.have I o Comment.ignore;
-val have_i    = local_statement_i true Proof.have_i I o Comment.ignore;
-val thus      = local_statement true Proof.show Proof.chain o Comment.ignore;
-val thus_i    = local_statement_i true Proof.show_i Proof.chain o Comment.ignore;
-val hence     = local_statement true Proof.have Proof.chain o Comment.ignore;
-val hence_i   = local_statement_i true Proof.have_i Proof.chain o Comment.ignore;
+val assume    = local_statement (Proof.assume assume_tac) I o Comment.ignore;
+val assume_i  = local_statement_i (Proof.assume_i assume_tac) I o Comment.ignore;
+val presume   = local_statement (Proof.assume (K all_tac)) I o Comment.ignore;
+val presume_i = local_statement_i (Proof.assume_i (K all_tac)) I o Comment.ignore;
+val show      = local_statement Proof.show I o Comment.ignore;
+val show_i    = local_statement_i Proof.show_i I o Comment.ignore;
+val have      = local_statement Proof.have I o Comment.ignore;
+val have_i    = local_statement_i Proof.have_i I o Comment.ignore;
+val thus      = local_statement Proof.show Proof.chain o Comment.ignore;
+val thus_i    = local_statement_i Proof.show_i Proof.chain o Comment.ignore;
+val hence     = local_statement Proof.have Proof.chain o Comment.ignore;
+val hence_i   = local_statement_i Proof.have_i Proof.chain o Comment.ignore;
 
 
 (* blocks *)
 
-val begin_block = ProofHistory.apply_open Proof.begin_block;
+val begin_block = ProofHistory.apply Proof.begin_block;
 val next_block = ProofHistory.apply Proof.next_block;
-val end_block = ProofHistory.apply_close Proof.end_block;
+val end_block = ProofHistory.apply Proof.end_block;
 
 
 (* backward steps *)
@@ -325,14 +324,14 @@
 (* local endings *)
 
 val local_qed =
-  proof'' o (ProofHistory.applys_close oo Method.local_qed) o apsome Comment.ignore_interest;
+  proof'' o (ProofHistory.applys oo Method.local_qed) o apsome Comment.ignore_interest;
 
 val local_terminal_proof =
-  proof'' o (ProofHistory.applys_close oo Method.local_terminal_proof) o Comment.ignore_interest;
+  proof'' o (ProofHistory.applys oo Method.local_terminal_proof) o Comment.ignore_interest;
 
-val local_immediate_proof = proof'' (ProofHistory.applys_close o Method.local_immediate_proof);
-val local_default_proof = proof'' (ProofHistory.applys_close o Method.local_default_proof);
-val local_skip_proof = proof'' (ProofHistory.applys_close o SkipProof.local_skip_proof);
+val local_immediate_proof = proof'' (ProofHistory.applys o Method.local_immediate_proof);
+val local_default_proof = proof'' (ProofHistory.applys o Method.local_default_proof);
+val local_skip_proof = proof'' (ProofHistory.applys o SkipProof.local_skip_proof);
 
 
 (* global endings *)