src/Pure/Isar/isar_cmd.ML
changeset 53171 a5e54d4d9081
parent 52549 802576856527
child 55828 42ac3cfb89f6
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Aug 23 20:09:34 2013 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Aug 23 20:35:50 2013 +0200
     1.3 @@ -265,12 +265,11 @@
     1.4    Proof.goal (Toplevel.proof_of (diag_state ctxt))
     1.5      handle Toplevel.UNDEF => error "No goal present";
     1.6  
     1.7 -val _ =
     1.8 -  Context.>> (Context.map_theory
     1.9 -   (ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "state"))
    1.10 -      (Scan.succeed "Isar_Cmd.diag_state ML_context") #>
    1.11 -    ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "goal"))
    1.12 -      (Scan.succeed "Isar_Cmd.diag_goal ML_context")));
    1.13 +val _ = Theory.setup
    1.14 +  (ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "state"))
    1.15 +    (Scan.succeed "Isar_Cmd.diag_state ML_context") #>
    1.16 +   ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "goal"))
    1.17 +    (Scan.succeed "Isar_Cmd.diag_goal ML_context"));
    1.18  
    1.19  
    1.20  (* print theorems *)