--- a/QuotMain.thy	Mon Nov 23 20:10:39 2009 +0100
+++ b/QuotMain.thy	Mon Nov 23 21:12:16 2009 +0100
@@ -1117,16 +1117,21 @@
 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 (@{term "Trueprop"} $ gl)
+    val all = if fastype_of gl = @{typ bool} then HOLogic.all_const else Term.all;
+    fun lambda_all (var as Free(_, T)) trm = (all T) $ lambda var trm;
+    val glv = fold lambda_all vars gl
+    val gla = (term_of o snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glv))
     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
+    if fastype_of gl = @{typ bool} then @{term Trueprop} $ glf else glf
   end
 *}
 
 
+ML {* atomize_goal @{theory} @{term "x memb [] = False"} *}
+ML {* atomize_goal @{theory} @{term "x = xa \<Longrightarrow> a # x = a # xa"} *}
+
+
 ML {*
 (* builds the relation for respects *)
  
@@ -1512,6 +1517,16 @@
 end
 *}
 
+ML {*
+fun lift_thm_goal_note lthy qty qty_name rsp_thms defs thm name goal =
+  let
+    val lifted_thm = lift_thm_goal lthy qty qty_name rsp_thms defs thm goal;
+    val (_, lthy2) = note (name, lifted_thm) lthy;
+  in
+    lthy2
+  end
+*}
+
 
 end