# HG changeset patch
# User chaieb
# Date 1183730967 -7200
# Node ID 6a8fb529b5428cf944ece2f53331154dadd52b4d
# Parent  60950b22dcbf473a1efe80412cbc511288fe6045
Tuned document

diff -r 60950b22dcbf -r 6a8fb529b542 src/HOL/ex/Reflection.thy
--- a/src/HOL/ex/Reflection.thy	Fri Jul 06 16:09:26 2007 +0200
+++ b/src/HOL/ex/Reflection.thy	Fri Jul 06 16:09:27 2007 +0200
@@ -17,7 +17,6 @@
   by (blast intro: ext)
 
 use "reflection.ML"
-ML{* Reify_Data.get @{context}*}
 
 method_setup reify = {*
   fn src =>