# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256728926 -3600
# Node ID 8934d21534693f4a0bd1a40bef98a023c660c378
# Parent  89a2ff3f82c779f0e4ca2ca7fd94dfbcded7b5ab
Fixed mistake in const generation, will postpone this.

diff -r 89a2ff3f82c7 -r 8934d2153469 FSet.thy
--- a/FSet.thy	Wed Oct 28 10:29:00 2009 +0100
+++ b/FSet.thy	Wed Oct 28 12:22:06 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 *}