# HG changeset patch
# User wenzelm
# Date 1378906212 -7200
# Node ID 4e9e150422d554611078e623b85b1559cd1c662c
# Parent  addbc2387c61d3a2815f5cecc27d05fedddde1b5
tuned whitespace;

diff -r addbc2387c61 -r 4e9e150422d5 src/HOL/ex/Adhoc_Overloading_Examples.thy
--- a/src/HOL/ex/Adhoc_Overloading_Examples.thy	Wed Sep 11 15:25:51 2013 +0200
+++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy	Wed Sep 11 15:30:12 2013 +0200
@@ -1,5 +1,5 @@
-(*  Title:  HOL/ex/Adhoc_Overloading_Examples.thy
-    Author: Christian Sternagel
+(*  Title:      HOL/ex/Adhoc_Overloading_Examples.thy
+    Author:     Christian Sternagel
 *)
 
 header {* Ad Hoc Overloading *}
diff -r addbc2387c61 -r 4e9e150422d5 src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML	Wed Sep 11 15:25:51 2013 +0200
+++ b/src/Tools/adhoc_overloading.ML	Wed Sep 11 15:30:12 2013 +0200
@@ -1,5 +1,5 @@
-(* Author: Alexander Krauss, TU Muenchen
-   Author: Christian Sternagel, University of Innsbruck
+(*  Author:     Alexander Krauss, TU Muenchen
+    Author:     Christian Sternagel, University of Innsbruck
 
 Adhoc overloading of constants based on their types.
 *)
@@ -21,6 +21,7 @@
 
 val show_variants = Attrib.setup_config_bool @{binding show_variants} (K false);
 
+
 (* errors *)
 
 fun err_duplicate_variant oconst =
@@ -48,6 +49,7 @@
           map (Pretty.mark Markup.item o Syntax.pretty_term ctxt') instances)))]))
   end;
 
+
 (* generic data *)
 
 fun variants_eq ((v1, T1), (v2, T2)) =
@@ -136,6 +138,7 @@
   val generic_remove_variant = generic_variant false;
 end;
 
+
 (* check / uncheck *)
 
 fun unifiable_with thy T1 T2 =
@@ -181,6 +184,7 @@
       | (cT :: _) => err_unresolved_overloading ctxt cT t (the_candidates cT));
   in map check_unresolved end;
 
+
 (* setup *)
 
 val _ = Context.>>
@@ -188,6 +192,7 @@
    #> Syntax_Phases.term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
    #> Syntax_Phases.term_uncheck 0 "adhoc_overloading" uncheck);
 
+
 (* commands *)
 
 fun generic_adhoc_overloading_cmd add =