--- a/src/Pure/Isar/proof.ML Thu Mar 05 11:11:42 2015 +0100
+++ b/src/Pure/Isar/proof.ML Thu Mar 05 13:28:04 2015 +0100
@@ -894,7 +894,6 @@
fun generic_goal prepp kind before_qed after_qed raw_propp state =
let
val ctxt = context_of state;
- val cert = Proof_Context.cterm_of ctxt;
val chaining = can assert_chain state;
val pos = Position.thread_data ();
@@ -910,7 +909,8 @@
val propss' = vars :: propss;
val goal_propss = filter_out null propss';
val goal =
- cert (Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss))
+ Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss)
+ |> Proof_Context.cterm_of ctxt
|> Thm.weaken_sorts (Variable.sorts_of (context_of goal_state));
val statement = ((kind, pos), propss', Thm.term_of goal);
val after_qed' = after_qed |>> (fn after_local =>