--- a/src/HOL/Tools/Function/partial_function.ML Wed Jul 08 15:37:32 2015 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Wed Jul 08 19:28:43 2015 +0200
@@ -230,7 +230,7 @@
val Setup_Data {fixp, mono, fixp_eq, fixp_induct, fixp_induct_user} = setup_data;
val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [eqn_raw] lthy;
- val ((_, plain_eqn), args_ctxt) = Variable.focus eqn lthy;
+ val ((_, plain_eqn), args_ctxt) = Variable.focus NONE eqn lthy;
val ((f_binding, fT), mixfix) = the_single fixes;
val fname = Binding.name_of f_binding;