--- a/src/HOL/Tools/Lifting/lifting_setup.ML Tue Jul 05 10:32:25 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Tue Jul 05 14:20:27 2016 +0200
@@ -96,7 +96,8 @@
(Binding.empty_atts, definition_term) lthy |>> (snd #> snd);
fun raw_def lthy =
let
- val ((_, rhs), prove) = Local_Defs.derived_def lthy {conditional = true} definition_term;
+ val ((_, rhs), prove) =
+ Local_Defs.derived_def lthy (K []) {conditional = true} definition_term;
val ((_, (_, raw_th)), lthy) =
Local_Theory.define
((Binding.concealed pcrel_name, NoSyn), (Binding.empty_atts, rhs)) lthy;