# HG changeset patch
# User wenzelm
# Date 1433856486 -7200
# Node ID 990c9fea67738f8b60337e4baf66aa14b679bb3d
# Parent  422b63ef01474985ce155c551949a84c6f3a4250
eliminated dead code;

diff -r 422b63ef0147 -r 990c9fea6773 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Jun 09 13:42:58 2015 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Jun 09 15:28:06 2015 +0200
@@ -173,17 +173,6 @@
   |> Context.proof_map;
 
 
-(* goals *)
-
-fun goal opt_chain goal stmt int =
-  opt_chain #> goal NONE (K I) stmt int;
-
-val have = goal I Proof.have_cmd;
-val hence = goal Proof.chain Proof.have_cmd;
-val show = goal I Proof.show_cmd;
-val thus = goal Proof.chain Proof.show_cmd;
-
-
 (* local endings *)
 
 fun local_qed m = Toplevel.proof (Proof.local_qed (m, true));