changeset 59573 | d09cc83cdce9 |
parent 59498 | 50b60f501b05 |
child 59621 | 291934bac95e |
--- a/src/Pure/Isar/local_defs.ML Sun Mar 01 14:15:49 2015 +0100 +++ b/src/Pure/Isar/local_defs.ML Sun Mar 01 23:35:41 2015 +0100 @@ -214,7 +214,7 @@ fun derived_def ctxt conditional prop = let val ((c, T), rhs) = prop - |> Thm.cterm_of (Proof_Context.theory_of ctxt) + |> Proof_Context.cterm_of ctxt |> meta_rewrite_conv ctxt |> (snd o Logic.dest_equals o Thm.prop_of) |> conditional ? Logic.strip_imp_concl