--- a/QuotMain.thy	Tue Oct 06 01:50:13 2009 +0200
+++ b/QuotMain.thy	Tue Oct 06 02:02:51 2009 +0200
@@ -737,17 +737,20 @@
   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
-
-  fun get_lhs [] = lhs
-    | get_lhs (x::xs) =  
-        let val cx = cterm_of (ProofContext.theory_of ctxt') (Free x)
-        in Thm.capply (get_lhs xs) cx end
+  
+  val thy = ProofContext.theory_of ctxt'
+  fun get_lhs xs = 
+  let 
+    val cxs = map (cterm_of thy o Free) xs
+  in
+    Drule.list_comb (lhs, cxs)
+  end
 
   fun get_conv [] = Conv.rewr_conv def
     | get_conv (x::xs) = Conv.fun_conv (get_conv xs)
  
 in
-  get_conv xs (get_lhs (rev xs)) |>  
+  get_conv xs (get_lhs xs) |>  
   singleton (ProofContext.export ctxt' ctxt)
 end
 *}