# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1258989199 -3600
# Node ID 959ef7f6ecdb7d209051659bdb6922eb54a2a86f
# Parent  573e2b625e8e68d8564631fc6dcdf211264bbe1f# Parent  0aba42afedad536e13ae7cf82c28e2e4c12ff921
merged

diff -r 573e2b625e8e -r 959ef7f6ecdb IntEx.thy
--- a/IntEx.thy	Mon Nov 23 16:12:50 2009 +0100
+++ b/IntEx.thy	Mon Nov 23 16:13:19 2009 +0100
@@ -181,6 +181,23 @@
 *}
 
 
+
+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 (@{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
+    term_of glac
+  end
+*}
+
+ML {* atomize_goal @{theory} @{term "PLUS a b = PLUS b a"} *}
+
+
 ML {*
 fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal =
 let
@@ -232,7 +249,7 @@
 *}
 
 ML {*
-  lift_thm_g_my_int @{context} @{thm plus_sym_pre} @{term "Trueprop (\<forall>a b. PLUS a b = PLUS b a)"}
+  lift_thm_g_my_int @{context} @{thm plus_sym_pre} @{term "PLUS a b = PLUS b a"}
 *}
 
 
@@ -401,3 +418,5 @@
 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_l *}
 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *}
 ML {* ObjectLogic.rulify t_r *}
+ML {* @{term "Trueprop"} *}
+
diff -r 573e2b625e8e -r 959ef7f6ecdb QuotMain.thy
--- a/QuotMain.thy	Mon Nov 23 16:12:50 2009 +0100
+++ b/QuotMain.thy	Mon Nov 23 16:13:19 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