# HG changeset patch
# User chaieb
# Date 1183890056 -7200
# Node ID 32ee4111d1bccd9094d1e0c90b4c09642ce2525d
# Parent  10672e025b83a1a380a00a1a69a2ed59e6c09e9e
Corrected erronus use of compiletime context to the runtime context

diff -r 10672e025b83 -r 32ee4111d1bc src/HOL/ex/reflection.ML
--- a/src/HOL/ex/reflection.ML	Sat Jul 07 18:47:47 2007 +0200
+++ b/src/HOL/ex/reflection.ML	Sun Jul 08 12:20:56 2007 +0200
@@ -268,7 +268,7 @@
   val cvs = map (fn (v as Var(n,t)) => (cert v, the (AList.lookup Type.could_unify (!bds) t) |> snd |> HOLogic.mk_list (dest_listT t) |> cert)) vars
   val th' = instantiate ([], cvs) th
   val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th'
-  val th'' = Goal.prove @{context} [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t')))
+  val th'' = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t')))
 			(fn _ => Simp_tac 1)
   val _ = bds := []
 in FWD trans [th'',th']