diff -r e6b96b4cde7e -r 0dec18004e75 src/Sequents/S43.thy
--- a/src/Sequents/S43.thy	Mon Sep 06 19:11:01 2010 +0200
+++ b/src/Sequents/S43.thy	Mon Sep 06 19:13:10 2010 +0200
@@ -79,12 +79,12 @@
 ML {*
 structure S43_Prover = Modal_ProverFun
 (
-  val rewrite_rls = thms "rewrite_rls"
-  val safe_rls = thms "safe_rls"
-  val unsafe_rls = thms "unsafe_rls" @ [thm "pi1", thm "pi2"]
-  val bound_rls = thms "bound_rls" @ [thm "boxL", thm "diaR"]
-  val aside_rls = [thm "lstar0", thm "lstar1", thm "lstar2", thm "rstar0",
-    thm "rstar1", thm "rstar2", thm "S43pi0", thm "S43pi1", thm "S43pi2"]
+  val rewrite_rls = @{thms rewrite_rls}
+  val safe_rls = @{thms safe_rls}
+  val unsafe_rls = @{thms unsafe_rls} @ [@{thm pi1}, @{thm pi2}]
+  val bound_rls = @{thms bound_rls} @ [@{thm boxL}, @{thm diaR}]
+  val aside_rls = [@{thm lstar0}, @{thm lstar1}, @{thm lstar2}, @{thm rstar0},
+    @{thm rstar1}, @{thm rstar2}, @{thm S43pi0}, @{thm S43pi1}, @{thm S43pi2}]
 )
 *}