--- a/src/HOL/HOLCF/Tools/cpodef.ML Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML Sun May 29 15:40:25 2016 +0200
@@ -175,7 +175,7 @@
Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))))
val ((_, (_, below_ldef)), lthy) = thy
|> Class.instantiation ([full_tname], lhs_tfrees, @{sort po})
- |> Specification.definition NONE []
+ |> Specification.definition NONE [] []
((Binding.prefix_name "below_" (Thm.def_binding name), []), below_eqn)
val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy)
val below_def = singleton (Proof_Context.export lthy ctxt_thy) below_ldef