# HG changeset patch
# User wenzelm
# Date 1257428847 -3600
# Node ID 181fae134b434afb9d9854132e7b705052582e43
# Parent  f5d95787224fe0ca82dd4e00e9e6cbe3f024a188
proper header;
eliminated SML97's opaque signature constrain, which is essentially a legacy feature (due to problems with ML toplevel pretty printing);

diff -r f5d95787224f -r 181fae134b43 src/HOLCF/Tools/adm_tac.ML
--- a/src/HOLCF/Tools/adm_tac.ML	Thu Nov 05 14:37:39 2009 +0100
+++ b/src/HOLCF/Tools/adm_tac.ML	Thu Nov 05 14:47:27 2009 +0100
@@ -1,4 +1,5 @@
-(*  Author:     Stefan Berghofer, TU Muenchen
+(*  Title:      HOLCF/Tools/adm_tac.ML
+    Author:     Stefan Berghofer, TU Muenchen
 
 Admissibility tactic.
 
@@ -18,7 +19,7 @@
   val adm_tac: Proof.context -> (int -> tactic) -> int -> tactic
 end;
 
-structure Adm :> ADM =
+structure Adm : ADM =
 struct