--- a/QuotMain.thy	Thu Oct 15 11:25:25 2009 +0200
+++ b/QuotMain.thy	Thu Oct 15 11:29:38 2009 +0200
@@ -544,6 +544,7 @@
        if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A))
      ) else z)"
 
+(* fold1_def is not usable, but: *)
 thm fold1.simps
 
 lemma cons_preserves:
@@ -560,39 +561,6 @@
   apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons QuotMain.m1)
   done
 
-
-text {*
-  Unabs_def converts a definition given as
-
-    c \<equiv> %x. %y. f x y
-
-  to a theorem of the form
-
-    c x y \<equiv> f x y
-
-  This function is needed to rewrite the right-hand
-  side to the left-hand side.
-*}
-
-ML {*
-fun unabs_def ctxt def =
-let
-  val (lhs, rhs) = Thm.dest_equals (cprop_of def)
-  val xs = strip_abs_vars (term_of rhs)
-  val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt
-  
-  val thy = ProofContext.theory_of ctxt'
-  val cxs = map (cterm_of thy o Free) xs
-  val new_lhs = Drule.list_comb (lhs, cxs)
-
-  fun get_conv [] = Conv.rewr_conv def
-    | get_conv (x::xs) = Conv.fun_conv (get_conv xs)
-in
-  get_conv xs new_lhs |>  
-  singleton (ProofContext.export ctxt' ctxt)
-end
-*}
-
 local_setup {*
   make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
@@ -601,11 +569,6 @@
 term IN
 thm IN_def
 
-(* unabs_def tests *)
-ML {* (Conv.fun_conv (Conv.fun_conv (Conv.rewr_conv @{thm IN_def}))) @{cterm "IN x y"} *}
-ML {* MetaSimplifier.rewrite_rule @{thms IN_def} @{thm IN_def}*}
-ML {* @{thm IN_def}; unabs_def @{context} @{thm IN_def} *}
-
 lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset]
 thm QUOT_TYPE.thm11[OF QUOT_TYPE_fset, THEN iffD1, simplified a]
 
@@ -774,6 +737,40 @@
 *}
 
 
+text {*
+  Unabs_def converts a definition given as
+
+    c \<equiv> %x. %y. f x y
+
+  to a theorem of the form
+
+    c x y \<equiv> f x y
+
+  This function is needed to rewrite the right-hand
+  side to the left-hand side.
+*}
+
+ML {*
+fun unabs_def ctxt def =
+let
+  val (lhs, rhs) = Thm.dest_equals (cprop_of def)
+  val xs = strip_abs_vars (term_of rhs)
+  val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt
+
+  val thy = ProofContext.theory_of ctxt'
+  val cxs = map (cterm_of thy o Free) xs
+  val new_lhs = Drule.list_comb (lhs, cxs)
+
+  fun get_conv [] = Conv.rewr_conv def
+    | get_conv (x::xs) = Conv.fun_conv (get_conv xs)
+in
+  get_conv xs new_lhs |>
+  singleton (ProofContext.export ctxt' ctxt)
+end
+*}
+
+ML {* (* Test: *) @{thm IN_def}; unabs_def @{context} @{thm IN_def} *}
+
 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
 ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *}