src/Pure/Isar/expression.ML
changeset 59573 d09cc83cdce9
parent 59296 002d817b4c37
child 59582 0fbed69ff081
     1.1 --- a/src/Pure/Isar/expression.ML	Sun Mar 01 14:15:49 2015 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Mar 01 23:35:41 2015 +0100
     1.3 @@ -758,7 +758,7 @@
     1.4  
     1.5  fun defines_to_notes ctxt (Defines defs) =
     1.6        Notes ("", map (fn (a, (def, _)) =>
     1.7 -        (a, [([Assumption.assume ctxt (cterm_of (Proof_Context.theory_of ctxt) def)],
     1.8 +        (a, [([Assumption.assume ctxt (Proof_Context.cterm_of ctxt def)],
     1.9            [(Attrib.internal o K) Locale.witness_add])])) defs)
    1.10    | defines_to_notes _ e = e;
    1.11