From e03cc0ba6b2a93341f7c59a7cbf6a61ef6a21788 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Fri, 20 Aug 2010 11:21:59 +0000
Subject: declare trace_simp in Isar, not ML;

---
 etc/isar/trace_simp.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/etc/isar/trace_simp.thy b/etc/isar/trace_simp.thy
index 1f56cb35..44f6e5af 100644
--- a/etc/isar/trace_simp.thy
+++ b/etc/isar/trace_simp.thy
@@ -6,7 +6,7 @@ text {*
   this produces massive amount of simplifier trace, but terminates
   eventually: *}
 
-ML {* Config.put trace_simp true *}
+declare [[trace_simp]]
 ML {* reset quick_and_dirty *}
 
 datatype ord = Zero | Succ ord | Limit "nat => ord"
-- 
cgit v1.2.3