--- a/QuotMain.thy	Mon Nov 23 15:08:25 2009 +0100
+++ b/QuotMain.thy	Mon Nov 23 15:47:14 2009 +0100
@@ -1118,7 +1118,7 @@
   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 gla = fold lambda_all vars (@{term "Trueprop"} $ gl)
     val glf = Type.legacy_freeze gla
     val glac = (snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glf))
   in