src/Cube/Cube.thy

--- a/src/Cube/Cube.thy	Fri Aug 15 18:02:34 2014 +0200
+++ b/src/Cube/Cube.thy	Sat Aug 16 11:35:33 2014 +0200
@@ -10,14 +10,7 @@
 
 setup Pure_Thy.old_appl_syntax_setup
 
-ML {*
-  structure Rules = Named_Thms
-  (
-    val name = @{binding rules}
-    val description = "Cube inference rules"
-  )
-*}
-setup Rules.setup
+named_theorems rules "Cube inference rules"
 
 typedecl "term"
 typedecl "context"