--- a/QuotMain.thy	Tue Sep 29 22:35:48 2009 +0200
+++ b/QuotMain.thy	Wed Sep 30 16:57:09 2009 +0200
@@ -831,10 +831,12 @@
 
 ML {* val qty = @{typ "'a fset"} *}
 ML {* val tt = Type ("fun", [Type ("fun", [qty, @{typ "prop"}]), @{typ "prop"}]) *}
-ML {* val fall = Const(@{const_name all}, tt) *}
+ML {* val fall = Const(@{const_name all}, dummyT) *}
+
+ML {* Syntax.check_term *}
 
 ML {*
-fun build_goal ctxt thm constructors rty qty mk_rep mk_abs =
+fun build_goal_term ctxt thm constructors rty qty mk_rep mk_abs =
   let
     fun mk_rep_abs x = mk_rep (mk_abs x);
 
@@ -851,6 +853,9 @@
     fun is_all (Const ("all", Type("fun", [Type("fun", [ty, _]), _]))) = ty = rty
       | is_all _ = false;
 
+    fun is_ex (Const ("Ex", Type("fun", [Type("fun", [ty, _]), _]))) = ty = rty
+      | is_ex _ = false;
+
     fun build_aux ctxt1 tm =
       let
         val (head, args) = Term.strip_comb tm;
@@ -873,22 +878,28 @@
               val t' = subst_bound (v, t);
               val rec_term = build_aux ctxt2 t';
             in Term.lambda_name (x, v) rec_term end
-        | _ =>
-            if is_all head then (* I assume that we never lift 'prop' since it is not of sort type *)
-              list_comb (fall, args')
+        | _ =>  (* I assume that we never lift 'prop' since it is not of sort type *)
+            if is_all head then
+              list_comb (Const(@{const_name all}, dummyT), args') |> Syntax.check_term ctxt1
+            else if is_ex head then
+              list_comb (Const(@{const_name Ex}, dummyT), args') |> Syntax.check_term ctxt1
             else if is_constructor head then
               maybe_mk_rep_abs (list_comb (head, map maybe_mk_rep_abs args'))
             else
               maybe_mk_rep_abs (list_comb (head, args'))
         )
       end;
-
-    val concl2 = Thm.prop_of thm;
   in
-    Logic.mk_equals (build_aux ctxt concl2, concl2)
+    build_aux ctxt (Thm.prop_of thm)
   end
 *}
 
+ML {*
+fun build_goal ctxt thm cons rty qty mk_rep mk_abs =
+  Logic.mk_equals ((build_goal_term ctxt thm cons rty qty mk_rep mk_abs), (Thm.prop_of thm))
+*}
+
+
 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
 ML {* val fset_defs_sym = map (fn t => symmetric (unlam_def @{context} t)) fset_defs *}
 
@@ -991,9 +1002,9 @@
       rtac @{thm QUOT_TYPE_I_fset.R_trans2},
       CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})),
       Cong_Tac.cong_tac @{thm cong},
-      rtac @{thm ext},
+      rtac @{thm ext}
 (*      rtac @{thm eq_reflection},*)
-      CHANGED o (ObjectLogic.full_atomize_tac)
+(*      CHANGED o (ObjectLogic.full_atomize_tac)*)
     ])
 *}
 
@@ -1029,6 +1040,7 @@
 
 prove {* (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
+  apply (atomize(full))
   apply (tactic {* foo_tac' @{context} 1 *})
   done
 
@@ -1041,6 +1053,7 @@
 *}
 prove {* Thm.term_of cgoal2 *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
+  apply (atomize(full))
   apply (tactic {* foo_tac' @{context} 1 *})
   sorry
 
@@ -1053,6 +1066,7 @@
 *}
 prove {* Thm.term_of cgoal2 *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
+  apply (atomize(full))
   apply (tactic {* foo_tac' @{context} 1 *})
   done
 
@@ -1068,6 +1082,7 @@
 (* It is the same, but we need a name for it. *)
 prove zzz : {* Thm.term_of cgoal3 *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
+  apply (atomize(full))
   apply (tactic {* foo_tac' @{context} 1 *})
   done
 
@@ -1095,6 +1110,7 @@
 *}
 prove {* Thm.term_of cgoal2 *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
+  apply (atomize(full))
   apply (tactic {* foo_tac' @{context} 1 *})
   done
 
@@ -1103,6 +1119,7 @@
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct}))
 *}
+
 ML {*
   val goal =
     Toplevel.program (fn () =>
@@ -1119,6 +1136,7 @@
 
 prove {* (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
+  apply (atomize(full))
   apply (tactic {* foo_tac' @{context} 1 *})
   sorry
 
@@ -1129,7 +1147,7 @@
       val goal = build_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs;
       val cgoal = cterm_of @{theory} goal;
       val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal);
-      val tac = (LocalDefs.unfold_tac @{context} fset_defs) THEN (foo_tac' @{context}) 1;
+      val tac = (LocalDefs.unfold_tac @{context} fset_defs) THEN (ObjectLogic.full_atomize_tac 1) THEN (foo_tac' @{context}) 1;
       val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac);
       val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm)))
       val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm;
@@ -1155,7 +1173,8 @@
 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *}
 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *}
 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *}
-(*local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*)
+(*ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} @{context}) *}
+local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*)
 
 thm m1_lift
 thm leqi4_lift
@@ -1222,11 +1241,10 @@
 ML {*  Thm.bicompose *}
 prove aaa: {* (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
+  apply (atomize(full))
   apply (tactic {* foo_tac' @{context} 1 *})
   done
 
-thm aaa
-
 (*
 datatype obj1 =
   OVAR1 "string"