src/Pure/Isar/proof.ML
changeset 59616 eb59c6968219
parent 59582 0fbed69ff081
child 59621 291934bac95e
     1.1 --- a/src/Pure/Isar/proof.ML	Thu Mar 05 11:11:42 2015 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Thu Mar 05 13:28:04 2015 +0100
     1.3 @@ -894,7 +894,6 @@
     1.4  fun generic_goal prepp kind before_qed after_qed raw_propp state =
     1.5    let
     1.6      val ctxt = context_of state;
     1.7 -    val cert = Proof_Context.cterm_of ctxt;
     1.8      val chaining = can assert_chain state;
     1.9      val pos = Position.thread_data ();
    1.10  
    1.11 @@ -910,7 +909,8 @@
    1.12      val propss' = vars :: propss;
    1.13      val goal_propss = filter_out null propss';
    1.14      val goal =
    1.15 -      cert (Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss))
    1.16 +      Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss)
    1.17 +      |> Proof_Context.cterm_of ctxt
    1.18        |> Thm.weaken_sorts (Variable.sorts_of (context_of goal_state));
    1.19      val statement = ((kind, pos), propss', Thm.term_of goal);
    1.20      val after_qed' = after_qed |>> (fn after_local =>