# HG changeset patch
# User wenzelm
# Date 1254172417 -7200
# Node ID 06c13b2e562ead03cb406c1f6b345351dddceae5
# Parent  71618deaf777d359cffb649dcbfebf245700ccf5
misc tuning and modernization;

diff -r 71618deaf777 -r 06c13b2e562e src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Sep 28 22:47:34 2009 +0200
+++ b/src/HOL/HOL.thy	Mon Sep 28 23:13:37 2009 +0200
@@ -1469,7 +1469,7 @@
 subsubsection {* Coherent logic *}
 
 ML {*
-structure Coherent = CoherentFun
+structure Coherent = Coherent
 (
   val atomize_elimL = @{thm atomize_elimL}
   val atomize_exL = @{thm atomize_exL}
diff -r 71618deaf777 -r 06c13b2e562e src/HOL/ex/Coherent.thy
--- a/src/HOL/ex/Coherent.thy	Mon Sep 28 22:47:34 2009 +0200
+++ b/src/HOL/ex/Coherent.thy	Mon Sep 28 23:13:37 2009 +0200
@@ -1,14 +1,15 @@
-(*  Title:      HOL/ex/Coherent
-    ID:         $Id$
+(*  Title:      HOL/ex/Coherent.thy
     Author:     Stefan Berghofer, TU Muenchen
-                Marc Bezem, Institutt for Informatikk, Universitetet i Bergen 
+    Author:     Marc Bezem, Institutt for Informatikk, Universitetet i Bergen 
 *)
 
-header{* Coherent Logic Problems *}
+header {* Coherent Logic Problems *}
 
-theory Coherent imports Main begin
+theory Coherent
+imports Main
+begin
 
-subsection{* Equivalence of two versions of Pappus' Axiom *}
+subsection {* Equivalence of two versions of Pappus' Axiom *}
 
 no_notation
   comp (infixl "o" 55) and
diff -r 71618deaf777 -r 06c13b2e562e src/Tools/coherent.ML
--- a/src/Tools/coherent.ML	Mon Sep 28 22:47:34 2009 +0200
+++ b/src/Tools/coherent.ML	Mon Sep 28 23:13:37 2009 +0200
@@ -26,7 +26,7 @@
   val setup: theory -> theory
 end;
 
-functor CoherentFun(Data: COHERENT_DATA) : COHERENT =
+functor Coherent(Data: COHERENT_DATA) : COHERENT =
 struct
 
 (** misc tools **)