--- a/src/HOL/Tools/Lifting/lifting_setup.ML Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Thu Apr 28 09:43:11 2016 +0200
@@ -89,8 +89,8 @@
val rhs = relcomp_op $ param_rel_fixed $ fixed_crel
val definition_term = Logic.mk_equals (lhs, rhs)
fun note_def lthy =
- Specification.definition ((SOME (pcrel_name, SOME relator_type, NoSyn)),
- ((Binding.empty, []), definition_term)) lthy |>> (snd #> snd);
+ Specification.definition (SOME (pcrel_name, SOME relator_type, NoSyn)) []
+ ((Binding.empty, []), definition_term) lthy |>> (snd #> snd);
fun raw_def lthy =
let
val ((_, rhs), prove) = Local_Defs.derived_def lthy {conditional = true} definition_term;