Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Corrected erronus use of compiletime context to the runtime context
authorchaieb
Sun, 08 Jul 2007 12:20:56 +0200
changeset 23643 32ee4111d1bc
parent 23642 10672e025b83
child 23644 e28b8e8a85b6
Corrected erronus use of compiletime context to the runtime context
src/HOL/ex/reflection.ML file | annotate | diff | comparison | revisions 
--- 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']
isabelle