src/HOL/ex/Commands.thy
changeset 59936 b8ffc3dc9e24
parent 59090 a0a05a4edb36
child 67096 e77f13a6a501
     1.1 --- a/src/HOL/ex/Commands.thy	Mon Apr 06 16:30:44 2015 +0200
     1.2 +++ b/src/HOL/ex/Commands.thy	Mon Apr 06 17:06:48 2015 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  subsection \<open>Diagnostic command: no state change\<close>
     1.5  
     1.6  ML \<open>
     1.7 -  Outer_Syntax.command @{command_spec "print_test"} "print term test"
     1.8 +  Outer_Syntax.command @{command_keyword print_test} "print term test"
     1.9      (Parse.term >> (fn s => Toplevel.keep (fn st =>
    1.10        let
    1.11          val ctxt = Toplevel.context_of st;
    1.12 @@ -30,7 +30,7 @@
    1.13  subsection \<open>Old-style global theory declaration\<close>
    1.14  
    1.15  ML \<open>
    1.16 -  Outer_Syntax.command @{command_spec "global_test"} "test constant declaration"
    1.17 +  Outer_Syntax.command @{command_keyword global_test} "test constant declaration"
    1.18      (Parse.binding >> (fn b => Toplevel.theory (fn thy =>
    1.19        let
    1.20          val thy' = Sign.add_consts [(b, @{typ 'a}, NoSyn)] thy;
    1.21 @@ -45,7 +45,7 @@
    1.22  subsection \<open>Local theory specification\<close>
    1.23  
    1.24  ML \<open>
    1.25 -  Outer_Syntax.local_theory @{command_spec "local_test"} "test local definition"
    1.26 +  Outer_Syntax.local_theory @{command_keyword local_test} "test local definition"
    1.27      (Parse.binding -- (@{keyword "="} |-- Parse.term) >> (fn (b, s) => fn lthy =>
    1.28        let
    1.29          val t = Syntax.read_term lthy s;