# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1251279115 -7200
# Node ID b11b405b8271c1a033cfac97358301d22352bce4
# Parent  eac147a5eb330f33da74688033715d36d0bb5286
Make both kinds of definitions.

diff -r eac147a5eb33 -r b11b405b8271 QuotMain.thy
--- a/QuotMain.thy	Tue Aug 25 17:37:50 2009 +0200
+++ b/QuotMain.thy	Wed Aug 26 11:31:55 2009 +0200
@@ -592,12 +592,23 @@
 apply(auto)
 done
 
-
-definition "IN x xa \<equiv> x memb REP_fset xa"
+ML {* 
+fun unlam_def t =
+  let
+    val (v, rest) = Thm.dest_abs NONE (Thm.rhs_of t)
+    val t2 = Drule.fun_cong_rule t v
+    val tnorm = equal_elim (Drule.beta_eta_conversion (Thm.cprop_of t2)) t2
+  in unlam_def tnorm end
+  handle CTERM _ => t
+*}
 
-(*local_setup {*
+local_setup {*
   make_const_def "IN" @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
-*}*)
+*}
+
+ML {* 
+  val IN_def = unlam_def @{thm IN_def}
+*}
 
 term membship
 term IN
@@ -719,7 +730,7 @@
 ML {* val emptyt = symmetric @{thm EMPTY_def} *}
 ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt] cgoal) *}
 
-ML {* val in_t = (symmetric @{thm IN_def}) *}
+ML {* val in_t = (symmetric IN_def) *}
 ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite false [in_t] (cgoal2)) *}
 
 (*theorem "(IN x EMPTY = False) = (x memb [] = False)"*)
@@ -729,5 +740,5 @@
 unfolding IN_def EMPTY_def
 apply (rule_tac mem_respects)
 apply (simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
-
-
+apply (simp_all)
+apply (rule list_eq_sym)