diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/Modal0.thy
--- a/src/Sequents/Modal0.thy	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/Modal0.thy	Sun Sep 18 15:20:08 2005 +0200
@@ -1,42 +1,43 @@
-(*  Title:      Sequents/Modal0
+(*  Title:      Sequents/Modal0.thy
     ID:         $Id$
     Author:     Martin Coen
     Copyright   1991  University of Cambridge
 *)
 
-Modal0 = LK0 +
+theory Modal0
+imports LK0
+uses "modal.ML"
+begin
 
 consts
   box           :: "o=>o"       ("[]_" [50] 50)
   dia           :: "o=>o"       ("<>_" [50] 50)
-  "--<",">-<"   :: "[o,o]=>o"   (infixr 25)
-  Lstar,Rstar   :: "two_seqi"
+  "--<"         :: "[o,o]=>o"   (infixr 25)
+  ">-<"         :: "[o,o]=>o"   (infixr 25)
+  Lstar         :: "two_seqi"
+  Rstar         :: "two_seqi"
 
 syntax
   "@Lstar"      :: "two_seqe"   ("(_)|L>(_)" [6,6] 5)
   "@Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
 
-rules
-  (* Definitions *)
-
-  strimp_def    "P --< Q == [](P --> Q)"
-  streqv_def    "P >-< Q == (P --< Q) & (Q --< P)"
-end
-
-ML
-
-local
-
+ML {*
   val Lstar = "Lstar";
   val Rstar = "Rstar";
   val SLstar = "@Lstar";
   val SRstar = "@Rstar";
 
-  fun star_tr c [s1,s2] =
-      Const(c,dummyT)$Sequents.seq_tr s1$Sequents.seq_tr s2;
-  fun star_tr' c [s1,s2] = 
-      Const(c,dummyT) $ Sequents.seq_tr' s1 $ Sequents.seq_tr' s2;
-in
-val parse_translation = [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)];
-val print_translation = [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)]
-end;
+  fun star_tr c [s1,s2] = Const(c,dummyT)$ seq_tr s1$ seq_tr s2;
+  fun star_tr' c [s1,s2] = Const(c,dummyT) $ seq_tr' s1 $ seq_tr' s2;
+*}
+
+parse_translation {* [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)] *}
+print_translation {* [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)] *}
+
+defs
+  strimp_def:    "P --< Q == [](P --> Q)"
+  streqv_def:    "P >-< Q == (P --< Q) & (Q --< P)"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
+end