changeset 59621 | 291934bac95e |
parent 59573 | d09cc83cdce9 |
child 59647 | c6f413b660cf |
--- a/src/Pure/Isar/local_defs.ML Fri Mar 06 14:01:08 2015 +0100 +++ b/src/Pure/Isar/local_defs.ML Fri Mar 06 15:58:56 2015 +0100 @@ -214,7 +214,7 @@ fun derived_def ctxt conditional prop = let val ((c, T), rhs) = prop - |> Proof_Context.cterm_of ctxt + |> Thm.cterm_of ctxt |> meta_rewrite_conv ctxt |> (snd o Logic.dest_equals o Thm.prop_of) |> conditional ? Logic.strip_imp_concl