src/Pure/Isar/isar_cmd.ML
changeset 60096 96a4765ba7d1
parent 60095 c48d536231fe
child 60099 d20ca79d50e4
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Apr 16 13:48:10 2015 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Apr 16 14:18:32 2015 +0200
     1.3 @@ -240,10 +240,7 @@
     1.4    in ML_Context.eval_source_in opt_ctxt flags source end);
     1.5  
     1.6  val diag_state = Diag_State.get;
     1.7 -
     1.8 -fun diag_goal ctxt =
     1.9 -  Proof.goal (Toplevel.proof_of (diag_state ctxt))
    1.10 -    handle Toplevel.UNDEF => error "No goal present";
    1.11 +val diag_goal = Proof.goal o Toplevel.proof_of o diag_state;
    1.12  
    1.13  val _ = Theory.setup
    1.14    (ML_Antiquotation.value (Binding.qualify true "Isar" @{binding state})