src/CCL/Term.thy
changeset 42814 5af15f1e2ef6
parent 42284 326f57825e1a
child 44241 7943b69f0188
--- a/src/CCL/Term.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/CCL/Term.thy	Sun May 15 17:45:53 2011 +0200
@@ -205,7 +205,7 @@
   Scan.succeed (fn ctxt =>
     SIMPLE_METHOD' (CHANGED o
       simp_tac (simpset_of ctxt addsimps @{thms rawBs} setloop (stac @{thm letrecB}))))
-*} ""
+*}
 
 lemma ifBtrue: "if true then t else u = t"
   and ifBfalse: "if false then t else u = u"