# HG changeset patch
# User chaieb
# Date 1183477795 -7200
# Node ID c8a1bd9585a086bcbbce286c3fe0e118a99fb566
# Parent  2fddae6056abe01801609cbbf21cc76a019d3e42
reflection and reification methods now manage Context data

diff -r 2fddae6056ab -r c8a1bd9585a0 src/HOL/ex/Reflection.thy
--- a/src/HOL/ex/Reflection.thy	Tue Jul 03 17:49:53 2007 +0200
+++ b/src/HOL/ex/Reflection.thy	Tue Jul 03 17:49:55 2007 +0200
@@ -7,26 +7,30 @@
 
 theory Reflection
 imports Main
-  uses ("reflection.ML")
+  uses "reflection_data.ML" ("reflection.ML")
 begin
 
+setup {* Reify_Data.setup*}
+
+
 lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
   by (blast intro: ext)
 
 use "reflection.ML"
+ML{* Reify_Data.get @{context}*}
 
 method_setup reify = {*
   fn src =>
     Method.syntax (Attrib.thms --
       Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
-  (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt eqs to))
+  (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ Reify_Data.get ctxt) to))
 *} "partial automatic reification"
 
 method_setup reflection = {*
   fn src =>
     Method.syntax (Attrib.thms --
       Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
-  (fn ((ths, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt ths to))
+  (fn ((ths, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt (ths @ Reify_Data.get ctxt) to))
 *} "reflection method"
 
 end