--- a/src/HOL/Basic_BNFs.thy Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Basic_BNFs.thy Mon Jan 20 18:24:56 2014 +0100
@@ -14,7 +14,6 @@
(*FIXME: define relators here, reuse in Lifting_* once this theory is in HOL*)
Lifting_Sum
Lifting_Product
- Main
begin
bnf ID: 'a