src/Pure/Isar/proof.ML

 in
 
 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 ();
 
     val ((propss, after_ctxt), goal_state) =
       state

 
     val vars = implicit_vars props;
     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 =>
       fn results => map_context after_ctxt #> after_local results);
   in