diff -r df05cd030d2f -r 329111e1c4ba FSet.thy
--- a/FSet.thy	Wed Oct 28 15:25:11 2009 +0100
+++ b/FSet.thy	Wed Oct 28 15:25:36 2009 +0100
@@ -169,14 +169,14 @@
 
 
 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *}
-ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *}
+(* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *)
 
-(* ML {*
+ML {*
   val consts = [@{const_name "Nil"}, @{const_name "Cons"},
                 @{const_name "membship"}, @{const_name "card1"},
                 @{const_name "append"}, @{const_name "fold1"},
                 @{const_name "map"}];
-*} *)
+*}
 
 ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *}