src/HOL/Decision_Procs/langford.ML

--- a/src/HOL/Decision_Procs/langford.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Decision_Procs/langford.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -171,7 +171,7 @@
 
 val reduce_ex_simproc =
   Simplifier.make_simproc @{context} "reduce_ex_simproc"
-    {lhss = [@{term "\<exists>x. P x"}], proc = K proc, identifier = []};
+    {lhss = [@{term "\<exists>x. P x"}], proc = K proc};
 
 end;