# HG changeset patch
# User haftmann
# Date 1392555408 -3600
# Node ID bd67ebe275e0bdfb4ff26606b6e1a8b166a67439
# Parent  90c42b1306525225914749799342765dbcb02f6e
eliminated odd dislocation of keyword declaration and implementation (leftover from 318cd8ac1817)

diff -r 90c42b130652 -r bd67ebe275e0 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Sat Feb 15 21:11:29 2014 +0100
+++ b/src/HOL/Groebner_Basis.thy	Sun Feb 16 13:56:48 2014 +0100
@@ -6,6 +6,7 @@
 
 theory Groebner_Basis
 imports Semiring_Normalization
+keywords "try0" :: diag
 begin
 
 subsection {* Groebner Bases *}
diff -r 90c42b130652 -r bd67ebe275e0 src/HOL/Metis.thy
--- a/src/HOL/Metis.thy	Sat Feb 15 21:11:29 2014 +0100
+++ b/src/HOL/Metis.thy	Sun Feb 16 13:56:48 2014 +0100
@@ -8,7 +8,6 @@
 
 theory Metis
 imports ATP
-keywords "try0" :: diag
 begin
 
 ML_file "~~/src/Tools/Metis/metis.ML"