diff -r 553bef083318 -r 62b188959c8a QuotMain.thy
--- a/QuotMain.thy	Mon Nov 23 14:05:02 2009 +0100
+++ b/QuotMain.thy	Mon Nov 23 14:16:41 2009 +0100
@@ -1206,6 +1206,20 @@
 (******************************************)
 
 ML {*
+fun atomize_goal thy gl =
+  let
+    val vars = map Free (Term.add_frees gl []);
+    fun lambda_all (var as Free(_, T)) trm = (Term.all T) $ lambda var trm;
+    val gla = fold lambda_all vars gl
+    val glf = Type.legacy_freeze gla
+    val glac = (snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glf))
+  in
+    term_of glac
+  end
+*}
+
+
+ML {*
 (* builds the relation for respects *)
  
 fun mk_resp_arg lthy (rty, qty) =