src/Pure/Isar/expression.ML
changeset 59582 0fbed69ff081
parent 59573 d09cc83cdce9
child 59616 eb59c6968219
     1.1 --- a/src/Pure/Isar/expression.ML	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Wed Mar 04 19:53:18 2015 +0100
     1.3 @@ -706,7 +706,7 @@
     1.4  fun define_preds binding parms (((exts, exts'), (ints, ints')), defs) thy =
     1.5    let
     1.6      val ctxt = Proof_Context.init_global thy;
     1.7 -    val defs' = map (cterm_of thy #> Assumption.assume ctxt #> Drule.abs_def) defs;
     1.8 +    val defs' = map (Thm.cterm_of thy #> Assumption.assume ctxt #> Drule.abs_def) defs;
     1.9  
    1.10      val (a_pred, a_intro, a_axioms, thy'') =
    1.11        if null exts then (NONE, NONE, [], thy)
    1.12 @@ -807,7 +807,7 @@
    1.13      val notes =
    1.14        if is_some asm then
    1.15          [("", [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) binding), []),
    1.16 -          [([Assumption.assume pred_ctxt (cterm_of thy' (the asm))],
    1.17 +          [([Assumption.assume pred_ctxt (Thm.cterm_of thy' (the asm))],
    1.18              [(Attrib.internal o K) Locale.witness_add])])])]
    1.19        else [];
    1.20