--- 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));