--- a/src/HOL/Metis_Examples/Binary_Tree.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Metis_Examples/Binary_Tree.thy Tue Sep 09 20:51:36 2014 +0200
@@ -13,7 +13,7 @@
declare [[metis_new_skolem]]
-datatype 'a bt =
+datatype_new 'a bt =
Lf
| Br 'a "'a bt" "'a bt"