--- a/QuotMain.thy	Thu Nov 05 09:38:34 2009 +0100
+++ b/QuotMain.thy	Thu Nov 05 09:55:21 2009 +0100
@@ -171,38 +171,6 @@
 
 section {* ATOMIZE *}
 
-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
-*}
-
 lemma atomize_eqv[atomize]: 
   shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" 
 proof