# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265019391 -3600
# Node ID cb03b34340e99ca58759a658b80f87ee38d206ba
# Parent  3f227ed7e3e54b6abfe4416fe945231828262302# Parent  9e3c8de7a61cbc93f76a68eaa2d9604e6bb0f4fe
merge

diff -r 3f227ed7e3e5 -r cb03b34340e9 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Mon Feb 01 11:16:13 2010 +0100
+++ b/Quot/Examples/IntEx.thy	Mon Feb 01 11:16:31 2010 +0100
@@ -186,13 +186,14 @@
   using a b c
   by (lifting int_induct_raw)
 
-lemma ex1tst: "Bexeq (op \<approx>) (\<lambda>x :: nat \<times> nat. x \<approx> x)"
+lemma ex1tst: "Bex1_rel (op \<approx>) (\<lambda>x :: nat \<times> nat. x \<approx> x)"
 sorry
 
-lemma ex1tst': "\<exists>! (x :: my_int). x = x"
+lemma ex1tst': "\<exists>!(x::my_int). x = x"
 apply(lifting ex1tst)
 done
 
+
 lemma ho_tst: "foldl my_plus x [] = x"
 apply simp
 done
diff -r 3f227ed7e3e5 -r cb03b34340e9 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Mon Feb 01 11:16:13 2010 +0100
+++ b/Quot/quotient_term.ML	Mon Feb 01 11:16:31 2010 +0100
@@ -388,7 +388,7 @@
 val mk_ball = Const (@{const_name Ball}, dummyT)
 val mk_bex  = Const (@{const_name Bex}, dummyT)
 val mk_bex1 = Const (@{const_name Bex1}, dummyT)
-val mk_bexeq = Const (@{const_name Bex1_rel}, dummyT)
+val mk_bex1_rel = Const (@{const_name Bex1_rel}, dummyT)
 val mk_resp = Const (@{const_name Respects}, dummyT)
 
 (* - applies f to the subterm of an abstraction, 
@@ -446,14 +446,14 @@
          if ty = ty' then subtrm
          else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
        end
-  | (Const (@{const_name "Babs"}, T) $ r $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) =>
+  | (Const (@{const_name "Babs"}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) =>
        let
          val subtrm = regularize_trm ctxt (t, t')
          val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty')
        in
-         if r <> needres
-         then term_mismatch "regularize (Babs)" ctxt r needres
-         else mk_babs $ r $ subtrm
+         if resrel <> needres
+         then term_mismatch "regularize (Babs)" ctxt resrel needres
+         else mk_babs $ resrel $ subtrm
        end
 
   | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
@@ -477,7 +477,7 @@
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
        in
          if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm
-         else mk_bexeq $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
+         else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
   | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, 
@@ -491,7 +491,6 @@
          else mk_ball $ (mk_resp $ resrel) $ subtrm
        end
 
-
   | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, 
      Const (@{const_name "Ex"}, ty') $ t') =>
        let
@@ -510,7 +509,7 @@
        in
          if resrel <> needrel
          then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel
-         else mk_bexeq $ resrel $ subtrm
+         else mk_bex1_rel $ resrel $ subtrm
        end
 
   | (Const (@{const_name "Bex1"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, 
@@ -521,7 +520,7 @@
        in
          if resrel <> needrel
          then term_mismatch "regularize (Bex1)" ctxt resrel needrel
-         else mk_bexeq $ resrel $ subtrm
+         else mk_bex1_rel $ resrel $ subtrm
        end
 
   | (* equalities need to be replaced by appropriate equivalence relations *) 
@@ -556,16 +555,16 @@
            end
        end 
 
-  | (((t1 as Const (@{const_name "split"}, _)) $ Abs(v1, ty, Abs(v1', ty', s1))),
-     ((t2 as Const (@{const_name "split"}, _)) $ Abs(v2, _ , Abs(v2', _  , s2)))) =>
-       (regularize_trm ctxt (t1, t2)) $ Abs(v1, ty, Abs(v1', ty', regularize_trm ctxt (s1, s2)))
+  | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
+     ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
+       regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
 
-  | (((t1 as Const (@{const_name "split"}, _)) $ Abs(v1, ty, s1)),
-     ((t2 as Const (@{const_name "split"}, _)) $ Abs(v2, _ , s2))) =>
-       (regularize_trm ctxt (t1, t2)) $ Abs(v1, ty, regularize_trm ctxt (s1, s2))
+  | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, s1)),
+     ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , s2))) =>
+       regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2))
 
   | (t1 $ t2, t1' $ t2') =>
-       (regularize_trm ctxt (t1, t1')) $ (regularize_trm ctxt (t2, t2'))
+       regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2')
 
   | (Bound i, Bound i') =>
        if i = i' then rtrm