# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259014143 -3600
# Node ID 9a0e8ab42ee8eb43ea311524132e156031f047e2
# Parent  28e312cfc80632d31226f841c89978da1552c8b1
fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)

diff -r 28e312cfc806 -r 9a0e8ab42ee8 FSet.thy
--- a/FSet.thy	Mon Nov 23 22:00:54 2009 +0100
+++ b/FSet.thy	Mon Nov 23 23:09:03 2009 +0100
@@ -311,29 +311,34 @@
 ML {* lift_thm_fset @{context} @{thm m1} *}
 ML {* lift_thm_g_fset @{context} @{thm m1} @{term "IN x EMPTY = False"} *}
 ML {* lift_thm_fset @{context} @{thm m2} *}
+
 ML {* lift_thm_g_fset @{context} @{thm m2} @{term "IN x (INSERT y xa) = (x = y \<or> IN x xa)"} *}
 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *}
 ML {* lift_thm_g_fset @{context} @{thm list_eq.intros(4)} @{term "INSERT a (INSERT a x) = INSERT a x"} *}
+
 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *}
 ML {* lift_thm_g_fset @{context} @{thm list_eq.intros(5)} @{term "x = xa \<Longrightarrow> INSERT a x = INSERT a xa"} *}
 ML {* lift_thm_fset @{context} @{thm card1_suc} *}
-ML {* lift_thm_g_fset @{context} @{thm card1_suc} @{term "CARD x = Suc n \<Longrightarrow> \<exists>a b. \<not> IN a b \<and> x = INSERT a b"} *}
+ML {* lift_thm_g_fset @{context} @{thm card1_suc} @{term "CARD x = Suc n \<Longrightarrow> \<exists>a b. \<not> IN a b \<and> x = INSERT a b"} *} 
 ML {* lift_thm_fset @{context} @{thm not_mem_card1} *}
 ML {* lift_thm_g_fset @{context} @{thm not_mem_card1} @{term "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"} *}
 ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *}
 (* Doesn't work with 'a, 'b, but works with 'b, 'a *)
+
 ML {* lift_thm_g_fset @{context} @{thm fold1.simps(2)} @{term "FOLD f g (z::'b) (INSERT a x) =
     (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 {* lift_thm_g_fset @{context} @{thm append_assoc} @{term "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"} *}
+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 {* val gl = @{term "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"} *}
 
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val rtrm = prop_of (atomize_thm @{thm map_append}) *}
+
 ML {* val qtrm = atomize_goal @{theory} gl *}
 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 *}
 
diff -r 28e312cfc806 -r 9a0e8ab42ee8 QuotMain.thy
--- a/QuotMain.thy	Mon Nov 23 22:00:54 2009 +0100
+++ b/QuotMain.thy	Mon Nov 23 23:09:03 2009 +0100
@@ -1146,9 +1146,6 @@
       (Type (s, tys), Type (s', tys')) =>
        if s = s' 
        then let
-              val _ = tracing ("maps lookup for  " ^ s)
-              val _ = tracing (Syntax.string_of_typ lthy rty)
-              val _ = tracing (Syntax.string_of_typ lthy qty)
               val SOME map_info = maps_lookup thy s
               val args = map (mk_resp_arg lthy) (tys ~~ tys')
             in
@@ -1158,8 +1155,11 @@
               val SOME qinfo = quotdata_lookup_thy thy s'
               (* FIXME: check in this case that the rty and qty *)
               (* FIXME: correspond to each other *)
+              val (s, _) = dest_Const (#rel qinfo)
+              (* FIXME: the relation should only be the string       *)
+              (* FIXME: and the type needs to be calculated as below *) 
             in
-              #rel qinfo
+              Const (s, rty --> rty --> @{typ bool})
             end
       | _ => HOLogic.eq_const dummyT 
              (* FIXME: check that the types correspond to each other? *)
@@ -1238,9 +1238,6 @@
   | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
        let
          val subtrm = apply_subt (REGULARIZE_trm lthy) t t'
-         val _ = tracing "quantor types All"
-         val _ = tracing (Syntax.string_of_typ lthy ty)
-         val _ = tracing (Syntax.string_of_typ lthy ty')
        in
          if ty = ty'
          then Const (@{const_name "All"}, ty) $ subtrm
@@ -1249,9 +1246,6 @@
   | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
        let
          val subtrm = apply_subt (REGULARIZE_trm lthy) t t'
-         val _ = tracing "quantor types Ex"
-         val _ = tracing (Syntax.string_of_typ lthy ty)
-         val _ = tracing (Syntax.string_of_typ lthy ty')
        in
          if ty = ty'
          then Const (@{const_name "Ex"}, ty) $ subtrm
diff -r 28e312cfc806 -r 9a0e8ab42ee8 quotient.ML
--- a/quotient.ML	Mon Nov 23 22:00:54 2009 +0100
+++ b/quotient.ML	Mon Nov 23 23:09:03 2009 +0100
@@ -153,8 +153,12 @@
   (* storing the quot-info *)
   val qty_str = fst (Term.dest_Type abs_ty)
   val _ = tracing ("storing under: " ^ qty_str)
-  val lthy3 = quotdata_update qty_str (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2  
+  val lthy3 = quotdata_update qty_str 
+               (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2  
   (* FIXME: varifyT should not be used *)
+  (* FIXME: the relation needs to be a string, since its type needs *)
+  (* FIXME: to recalculated in for example REGULARIZE *)
+
   (* storing of the equiv_thm under a name *)
   val (_, lthy4) = note (Binding.suffix_name "_equiv" qty_name, equiv_thm) lthy3