--- a/src/Pure/theory.ML Sun Apr 24 20:29:49 2016 +0200
+++ b/src/Pure/theory.ML Sun Apr 24 20:37:24 2016 +0200
@@ -291,7 +291,7 @@
fun check_def (context as (ctxt, _)) thy unchecked overloaded (b, tm) defs =
let
val name = Sign.full_name thy b;
- val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
+ val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (SOME (K false)) (K false) tm
handle TERM (msg, _) => error msg;
val lhs_const = Term.dest_Const (Term.head_of lhs);