# HG changeset patch
# User wenzelm
# Date 1291738994 -3600
# Node ID c78a2d402736ee3339a721376c13b67055a0980b
# Parent  3890ef4e02f9fec9e0d7f3a33ad4a1bb73ce52fa
eliminated some hard tabulators (deprecated);

diff -r 3890ef4e02f9 -r c78a2d402736 src/HOL/Mutabelle/mutabelle.ML
--- a/src/HOL/Mutabelle/mutabelle.ML	Tue Dec 07 16:27:07 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML	Tue Dec 07 17:23:14 2010 +0100
@@ -637,9 +637,9 @@
 
 fun create_spaces entry spacenum =
  let 
-		val diff = spacenum - (size entry)
- in 
-		if (diff > 0) 
+   val diff = spacenum - (size entry)
+ in
+   if (diff > 0)
    then implode (replicate diff " ")
    else ""
  end;
@@ -756,7 +756,7 @@
  end;
 
 (*exchange version of function mutqc_thystat*)
-			
+
 fun mutqc_thystat_exc p mutthy usedthy commutatives iter insts sz qciter filename =
  mutqc_thystat 0 p mutthy usedthy commutatives [] iter insts sz qciter filename;
 
diff -r 3890ef4e02f9 -r c78a2d402736 src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Tue Dec 07 16:27:07 2010 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy	Tue Dec 07 17:23:14 2010 +0100
@@ -1120,18 +1120,18 @@
       have b: "l \<approx> r" by fact
       have d: "card_list l = Suc m" by fact
       then have "\<exists>a. List.member l a" 
-	apply(simp)
-	apply(drule card_eq_SucD)
-	apply(blast)
-	done
+        apply(simp)
+        apply(drule card_eq_SucD)
+        apply(blast)
+        done
       then obtain a where e: "List.member l a" by auto
       then have e': "List.member r a" using list_eq_def [simplified List.member_def [symmetric], of l r] b 
-	by auto
+        by auto
       have f: "card_list (removeAll a l) = m" using e d by (simp)
       have g: "removeAll a l \<approx> removeAll a r" using removeAll_rsp b by simp
       have "(removeAll a l) \<approx>2 (removeAll a r)" by (rule Suc.hyps[OF f g])
       then have h: "(a # removeAll a l) \<approx>2 (a # removeAll a r)" by (rule list_eq2.intros(5))
-      have i: "l \<approx>2 (a # removeAll a l)"	
+      have i: "l \<approx>2 (a # removeAll a l)"
         by (rule list_eq2.intros(3)[OF member_delete_list_eq2[OF e]])
       have "l \<approx>2 (a # removeAll a r)" by (rule list_eq2.intros(6)[OF i h])
       then show ?case using list_eq2.intros(6)[OF _ member_delete_list_eq2[OF e']] by simp
diff -r 3890ef4e02f9 -r c78a2d402736 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Tue Dec 07 16:27:07 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Tue Dec 07 17:23:14 2010 +0100
@@ -755,7 +755,7 @@
   "#!/usr/bin/swipl -q -t main -f\n\n" ^
   ":- use_module(library('dialect/ciao/aggregates')).\n" ^
   ":- style_check(-singleton).\n" ^
-  ":- style_check(-discontiguous).\n" ^ 	
+  ":- style_check(-discontiguous).\n" ^
   ":- style_check(-atom).\n\n" ^
   "main :- catch(eval, E, (print_message(error, E), fail)), halt.\n" ^
   "main :- halt(1).\n"
diff -r 3890ef4e02f9 -r c78a2d402736 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Tue Dec 07 16:27:07 2010 +0100
+++ b/src/Pure/pattern.ML	Tue Dec 07 17:23:14 2010 +0100
@@ -365,7 +365,7 @@
   and cases(binders,env as (iTs,itms),pat,obj) =
     let val (ph,pargs) = strip_comb pat
         fun rigrig1(iTs,oargs) = fold (mtch binders) (pargs~~oargs) (iTs,itms)
-				 handle ListPair.UnequalLengths => raise MATCH
+          handle ListPair.UnequalLengths => raise MATCH
         fun rigrig2((a:string,Ta),(b,Tb),oargs) =
               if a <> b then raise MATCH
               else rigrig1(typ_match thy (Ta,Tb) iTs, oargs)