# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1265796666 -3600
# Node ID f24e9d21a948912be56f208aa3a9ac7dfaefcfc3
# Parent  67dff6c1a1238e77dc2a7524a4a5797028116a92# Parent  9f6c606d5b594300e519bd0e17d0a9042b922e44
merged again

diff -r 67dff6c1a123 -r f24e9d21a948 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Wed Feb 10 11:10:44 2010 +0100
+++ b/Quot/QuotMain.thy	Wed Feb 10 11:11:06 2010 +0100
@@ -140,7 +140,7 @@
   shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"
   and   QT_ex:  "Quot_True (Ex P) \<Longrightarrow> Quot_True P"
   and   QT_ex1: "Quot_True (Ex1 P) \<Longrightarrow> Quot_True P"
-  and   QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True  (P x))"
+  and   QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True (P x))"
   and   QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)"
 by (simp_all add: Quot_True_def ext)
 
@@ -169,7 +169,7 @@
   {* Sets up the three goals for the lifting procedure. *}
 
 method_setup regularize =
-  {* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac)  *}
+  {* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac) *}
   {* Proves automatically the regularization goals from the lifting procedure. *}
 
 method_setup injection =
diff -r 67dff6c1a123 -r f24e9d21a948 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Wed Feb 10 11:10:44 2010 +0100
+++ b/Quot/quotient_tacs.ML	Wed Feb 10 11:11:06 2010 +0100
@@ -29,7 +29,7 @@
 
 (* Since HOL_basic_ss is too "big" for us, we *)
 (* need to set up our own minimal simpset.    *)
-fun  mk_minimal_ss ctxt =
+fun mk_minimal_ss ctxt =
   Simplifier.context ctxt empty_ss
     setsubgoaler asm_simp_tac
     setmksimps (mksimps [])
diff -r 67dff6c1a123 -r f24e9d21a948 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Wed Feb 10 11:10:44 2010 +0100
+++ b/Quot/quotient_term.ML	Wed Feb 10 11:11:06 2010 +0100
@@ -90,7 +90,7 @@
       TVar _ => mk_Free rty
     | Type (_, []) => mk_identity rty
     | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
-    | _ => raise LIFT_MATCH ("mk_mapfun (default)")
+    | _ => raise LIFT_MATCH "mk_mapfun (default)"
 in
   fold_rev Term.lambda vs' (mk_mapfun_aux rty)
 end
@@ -706,7 +706,7 @@
       | x => x)
 
 (* subst_trms takes a list of (rtrm, qtrm) substitution pairs
-   and if the  given term matches any of the raw terms it
+   and if the given term matches any of the raw terms it
    returns the appropriate qtrm instantiated. If none of
    them matched it returns NONE. *)
 fun subst_trm thy t (rtrm, qtrm) s =