tuned;
authorwenzelm
Tue Jun 21 17:35:45 2016 +0200 (2016-06-21)
changeset 6334249fa6aaa4529
parent 63341 40f58bb9c846
child 63343 fb5d8a50c641
tuned;
src/HOL/Tools/BNF/bnf_gfp_grec.ML
src/HOL/Tools/Lifting/lifting_def_code_dt.ML
src/HOL/Tools/record.ML
src/Pure/Pure.thy
     1.1 --- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Tue Jun 21 17:25:28 2016 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Tue Jun 21 17:35:45 2016 +0200
     1.3 @@ -525,7 +525,7 @@
     1.4              val T = qsoty (unfreeze_fp Y);
     1.5              val T_backdrop = qsoty (unfreeze_fp Y_backdrop);
     1.6              fun register_hint () =
     1.7 -              "\nUse the " ^ quote (#1 @{command_keyword "bnf"}) ^ " command to register " ^
     1.8 +              "\nUse the " ^ quote (#1 @{command_keyword bnf}) ^ " command to register " ^
     1.9                quote bad_tc ^ " as a bounded natural functor to allow nested (co)recursion through \
    1.10                \it";
    1.11            in
     2.1 --- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Tue Jun 21 17:25:28 2016 +0200
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Tue Jun 21 17:35:45 2016 +0200
     2.3 @@ -810,7 +810,7 @@
     2.4  (* command syntax *)
     2.5  
     2.6  val _ =
     2.7 -  Outer_Syntax.local_theory_to_proof @{command_keyword "lift_definition"}
     2.8 +  Outer_Syntax.local_theory_to_proof @{command_keyword lift_definition}
     2.9      "definition for constants over the quotient type"
    2.10      (parse_params --
    2.11        (((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix')
     3.1 --- a/src/HOL/Tools/record.ML	Tue Jun 21 17:25:28 2016 +0200
     3.2 +++ b/src/HOL/Tools/record.ML	Tue Jun 21 17:35:45 2016 +0200
     3.3 @@ -2415,7 +2415,7 @@
     3.4    Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) []
     3.5  
     3.6  val _ =
     3.7 -  Outer_Syntax.command @{command_keyword "print_record"} "print record definiton"
     3.8 +  Outer_Syntax.command @{command_keyword print_record} "print record definiton"
     3.9      (opt_modes -- Parse.typ >> print_record);
    3.10  
    3.11  end
     4.1 --- a/src/Pure/Pure.thy	Tue Jun 21 17:25:28 2016 +0200
     4.2 +++ b/src/Pure/Pure.thy	Tue Jun 21 17:35:45 2016 +0200
     4.3 @@ -869,7 +869,7 @@
     4.4      (Scan.succeed Isar_Cmd.skip_proof);
     4.5  
     4.6  val _ =
     4.7 -  Outer_Syntax.command @{command_keyword "\<proof>"} "dummy proof (quick-and-dirty mode only!)"
     4.8 +  Outer_Syntax.command @{command_keyword \<proof>} "dummy proof (quick-and-dirty mode only!)"
     4.9      (Scan.succeed Isar_Cmd.skip_proof);
    4.10  
    4.11  val _ =