Mercurial Mercurial > hg > nominal2 / 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.
merge
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Mon, 08 Feb 2010 13:04:29 +0100
changeset 1086 ab5789ad8d7d
parent 1085 cf53861a00a7 (current diff)
parent 1084 40e3e6a6076f (diff)
child 1088 480324a48a1c
merge
--- a/Quot/quotient_tacs.ML	Mon Feb 08 13:04:13 2010 +0100
+++ b/Quot/quotient_tacs.ML	Mon Feb 08 13:04:29 2010 +0100
@@ -654,10 +654,9 @@
   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 [nthm1] = ProofContext.export ctxt' ctxt [nthm]
 in
-  nthm1
+  Goal.prove ctxt' [] [] goal (K (lift_tac ctxt' [thm] 1))
+  |> singleton (ProofContext.export ctxt' ctxt)
 end;
 
 val lifted_attrib = Thm.rule_attribute lifted_attrib_aux
nominal2