src/Pure/Isar/expression.ML
changeset 59616 eb59c6968219
parent 59582 0fbed69ff081
child 59621 291934bac95e
     1.1 --- a/src/Pure/Isar/expression.ML	Thu Mar 05 11:11:42 2015 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu Mar 05 13:28:04 2015 +0100
     1.3 @@ -678,18 +678,17 @@
     1.4          [((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
     1.5      val defs_ctxt = Proof_Context.init_global defs_thy |> Variable.declare_term head;
     1.6  
     1.7 -    val cert = Thm.cterm_of defs_thy;
     1.8 -
     1.9      val intro = Goal.prove_global defs_thy [] norm_ts statement
    1.10        (fn {context = ctxt, ...} =>
    1.11          rewrite_goals_tac ctxt [pred_def] THEN
    1.12          compose_tac defs_ctxt (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
    1.13          compose_tac defs_ctxt
    1.14 -          (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
    1.15 +          (false,
    1.16 +            Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_thy) norm_ts), 0) 1);
    1.17  
    1.18      val conjuncts =
    1.19        (Drule.equal_elim_rule2 OF
    1.20 -        [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (cert statement))])
    1.21 +        [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (Thm.cterm_of defs_thy statement))])
    1.22        |> Conjunction.elim_balanced (length ts);
    1.23  
    1.24      val (_, axioms_ctxt) = defs_ctxt