# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1258798608 -3600
# Node ID 3d7a3a1419221bf79f761f487a9f26d76f78112f
# Parent  bdbb529797908ccc94cf18e4c1ae83753d66120d
tuned

diff -r bdbb52979790 -r 3d7a3a141922 QuotMain.thy
--- a/QuotMain.thy	Sat Nov 21 10:58:08 2009 +0100
+++ b/QuotMain.thy	Sat Nov 21 11:16:48 2009 +0100
@@ -1200,8 +1200,10 @@
 *}
 
 (******************************************)
+(******************************************)
 (* version with explicit qtrm             *)
 (******************************************)
+(******************************************)
 
 ML {*
 fun mk_resp_arg lthy (rty, qty) =
@@ -1238,7 +1240,7 @@
 let
   val rtrm_str = quote (Syntax.string_of_term lthy rtrm) 
   val qtrm_str = quote (Syntax.string_of_term lthy qtrm)
-  val msg = ["quotient theorem", qtrm_str, "and lifted theorem", rtrm_str, "do not match."]
+  val msg = ["The quotient theorem", qtrm_str, "and lifted theorem", rtrm_str, "do not match."]
 in
   raise LIFT_MATCH (space_implode " " msg)
 end 
@@ -1274,13 +1276,13 @@
 ML {*
 fun REGULARIZE_trm lthy rtrm qtrm =
   case (rtrm, qtrm) of
-    (Abs (x, T, t), Abs (x', T', t')) =>
+    (Abs (x, ty, t), Abs (x', ty', t')) =>
        let
          val subtrm = REGULARIZE_trm lthy t t'
        in     
-         if T = T'
-         then Abs (x, T, subtrm)
-         else  mk_babs $ (mk_resp $ mk_resp_arg lthy (T, T')) $ subtrm
+         if ty = ty'
+         then Abs (x, ty, subtrm)
+         else  mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm
        end
   | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
        let
@@ -1298,7 +1300,7 @@
          then Const (@{const_name "Ex"}, ty) $ subtrm
          else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
-  (* FIXME: why is there a case for equality? is it correct? *)
+  (* FIXME: Why is there a case for equality? Is it correct? *)
   | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') =>
        let
          val subtrm = REGULARIZE_trm lthy t t'
@@ -1361,8 +1363,7 @@
 
 ML {*
 fun REGULARIZE_tac lthy rel_refl rel_eqv =
-  ObjectLogic.full_atomize_tac THEN'
-   REPEAT_ALL_NEW (FIRST' 
+   (REPEAT1 o FIRST1) 
      [rtac rel_refl,
       atac,
       rtac @{thm universal_twice},
@@ -1372,7 +1373,7 @@
       rtac (rel_eqv RS @{thm my_equiv_res_exists}),
       (* For a = b \<longrightarrow> a \<approx> b *)
       rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl,
-      rtac @{thm RIGHT_RES_FORALL_REGULAR}])
+      rtac @{thm RIGHT_RES_FORALL_REGULAR}]
 *}
 
 (* same version including debugging information *)
@@ -1411,7 +1412,7 @@
   let
     val goal = mk_REGULARIZE_goal lthy rtrm qtrm
     val cthm = Goal.prove lthy [] [] goal 
-      (fn {context, ...} => REGULARIZE_tac context rel_refl rel_eqv 1)
+      (fn {context, ...} => REGULARIZE_tac' context rel_refl rel_eqv)
   in
     cthm 
   end
diff -r bdbb52979790 -r 3d7a3a141922 quotient_def.ML
--- a/quotient_def.ML	Sat Nov 21 10:58:08 2009 +0100
+++ b/quotient_def.ML	Sat Nov 21 11:16:48 2009 +0100
@@ -147,7 +147,6 @@
   quotdef ((bind, qty, mx), (attr, prop)) lthy |> snd
 end
 
-
 val quotdef_parser =
   (OuterParse.binding --
     (OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.typ --