src/Pure/Isar/isar_cmd.ML
changeset 56204 f70e69208a8c
parent 56158 c2c6d560e7b2
child 56275 600f432ab556
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Mar 18 13:36:28 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Mar 18 15:29:58 2014 +0100
     1.3 @@ -247,9 +247,9 @@
     1.4      handle Toplevel.UNDEF => error "No goal present";
     1.5  
     1.6  val _ = Theory.setup
     1.7 -  (ML_Antiquotation.value (Binding.qualify true "Isar" (Binding.name "state"))
     1.8 +  (ML_Antiquotation.value (Binding.qualify true "Isar" @{binding state})
     1.9      (Scan.succeed "Isar_Cmd.diag_state ML_context") #>
    1.10 -   ML_Antiquotation.value (Binding.qualify true "Isar" (Binding.name "goal"))
    1.11 +   ML_Antiquotation.value (Binding.qualify true "Isar" @{binding goal})
    1.12      (Scan.succeed "Isar_Cmd.diag_goal ML_context"));
    1.13  
    1.14