src/HOL/Tools/refute_isar.ML
changeset 17057 0934ac31985f
parent 15570 8d8c70b41bab
child 17273 e95f7141ba2f
--- a/src/HOL/Tools/refute_isar.ML	Tue Aug 16 13:42:23 2005 +0200
+++ b/src/HOL/Tools/refute_isar.ML	Tue Aug 16 13:42:26 2005 +0200
@@ -54,7 +54,7 @@
 
 	fun refute_parser tokens = (refute_scan_args tokens) |>> refute_trans;
 
-	val refute_cmd = OuterSyntax.improper_command "refute" "try to find a model that refutes a given subgoal" OuterSyntax.Keyword.diag refute_parser;
+	val refute_cmd = OuterSyntax.improper_command "refute" "try to find a model that refutes a given subgoal" OuterKeyword.diag refute_parser;
 
 (* ------------------------------------------------------------------------- *)
 (* set up the 'refute_params' command                                        *)
@@ -90,7 +90,7 @@
 
 	fun refute_params_parser tokens = (refute_params_scan_args tokens) |>> refute_params_trans;
 
-	val refute_params_cmd = OuterSyntax.command "refute_params" "show/store default parameters for the 'refute' command" OuterSyntax.Keyword.thy_decl refute_params_parser;
+	val refute_params_cmd = OuterSyntax.command "refute_params" "show/store default parameters for the 'refute' command" OuterKeyword.thy_decl refute_params_parser;
 
 end;