src/Pure/Isar/isar_cmd.ML
changeset 56072 31e427387ab5
parent 56006 6a4dcaf53664
child 56155 1b9c089ed12d
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Mar 12 22:44:55 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Mar 12 22:57:50 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_Antiquote.value (Binding.qualify true "Isar" (Binding.name "state"))
     1.8 +  (ML_Antiquotation.value (Binding.qualify true "Isar" (Binding.name "state"))
     1.9      (Scan.succeed "Isar_Cmd.diag_state ML_context") #>
    1.10 -   ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "goal"))
    1.11 +   ML_Antiquotation.value (Binding.qualify true "Isar" (Binding.name "goal"))
    1.12      (Scan.succeed "Isar_Cmd.diag_goal ML_context"));
    1.13  
    1.14