Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/quotient_tacs.ML
changeset 1083 30550327651a
parent 1082 f8029d8c88a9
child 1084 40e3e6a6076f 
--- a/Quot/quotient_tacs.ML	Mon Feb 08 10:47:19 2010 +0100
+++ b/Quot/quotient_tacs.ML	Mon Feb 08 11:41:25 2010 +0100
@@ -653,8 +653,8 @@
 let
   val ctxt = Context.proof_of context
   val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt
-  val goal = (quotient_lift_all ctxt o prop_of) thm'
-  val nthm = Goal.prove ctxt [] [] goal (fn x => lift_tac ctxt [thm] 1)
+  val goal = (quotient_lift_all ctxt' o prop_of) thm'
+  val nthm = Goal.prove ctxt' [] [] goal (fn x => lift_tac ctxt' [thm] 1)
   val [nthm1] = ProofContext.export ctxt' ctxt [nthm]
 in
   nthm1
nominal2