src/HOL/Data_Structures/Define_Time_0.ML
changeset 79969 4aeb25ba90f3
parent 79490 b287510a4202
--- a/src/HOL/Data_Structures/Define_Time_0.ML	Sun Mar 24 14:15:10 2024 +0100
+++ b/src/HOL/Data_Structures/Define_Time_0.ML	Sun Mar 24 14:50:47 2024 +0100
@@ -37,7 +37,7 @@
 end
 
 val _ =
-  Outer_Syntax.command \<^command_keyword>\<open>define_time_0\<close> "ML setup for global theory"
+  Outer_Syntax.command \<^command_keyword>\<open>time_fun_0\<close> "ML setup for global theory"
     (Parse.prop >> (Toplevel.theory o save));
 
 end
\ No newline at end of file