# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259009324 -3600
# Node ID f507f088de73573b291436d6c3eb5c977a95b247
# Parent  b1f83c7a8674c33b2942af112b739060f2f05c01
domain_type in regularizing equality

diff -r b1f83c7a8674 -r f507f088de73 FSet.thy
--- a/FSet.thy	Mon Nov 23 21:12:16 2009 +0100
+++ b/FSet.thy	Mon Nov 23 21:48:44 2009 +0100
@@ -326,22 +326,24 @@
     (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"} *}
 
 ML {* lift_thm_fset @{context} @{thm append_assoc} *}
-ML {* val goal_a = atomize_goal @{theory} @{term "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"} *}
-ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
-(* Fails *)
-ML {* val reg_trm = mk_REGULARIZE_goal @{context} (prop_of (atomize_thm @{thm append_assoc})) goal_a *}
+ML {* lift_thm_g_fset @{context} @{thm append_assoc} @{term "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"} *}
+ML {* lift_thm_fset @{context} @{thm map_append} *}
+ML {* lift_thm_g_fset @{context} @{thm map_append} @{term "fmap f (FUNION x xa) = FUNION (fmap f x) (fmap f xa)"} *}
+
+ML {* lift_thm_fset @{context} @{thm list.induct} *}
+ML {* lift_thm_g_fset @{context} @{thm list.induct} @{term "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"} *}
 
 
-
-
+ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
+ML {* val rtrm = prop_of (atomize_thm @{thm append_assoc}) *}
+ML {* val qtrm = goal_a *}
+ML {* val a = (REGULARIZE_trm @{context} rtrm qtrm) *}
+ML {* val a = Syntax.check_term @{context} a *}
 ML {* val t_r = regularize_goal @{context} (atomize_thm @{thm append_assoc}) rel_eqv rel_refl goal_a *}
 
 ML {* lift_thm_g_fset @{context} @{thm append_assoc} gl *}
 
 
-ML {* lift_thm_fset @{context} @{thm map_append} *}
-ML {* lift_thm_fset @{context} @{thm list.induct} *}
-ML {* lift_thm_g_fset @{context} @{thm list.induct} @{term "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"} *}
 
 (*ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *}*)
 
diff -r b1f83c7a8674 -r f507f088de73 QuotMain.thy
--- a/QuotMain.thy	Mon Nov 23 21:12:16 2009 +0100
+++ b/QuotMain.thy	Mon Nov 23 21:48:44 2009 +0100
@@ -1264,7 +1264,7 @@
        in
          if ty = ty'
          then Const (@{const_name "op ="}, ty) $ subtrm
-         else mk_resp_arg lthy (ty, ty') $ subtrm
+         else mk_resp_arg lthy (domain_type ty, domain_type ty') $ subtrm
        end 
   | (t1 $ t2, t1' $ t2') =>
        (REGULARIZE_trm lthy t1 t1') $ (REGULARIZE_trm lthy t2 t2')