src/HOL/Statespace/distinct_tree_prover.ML

--- a/src/HOL/Statespace/distinct_tree_prover.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -360,8 +360,7 @@
         Const (@{const_name HOL.eq}, _) $ x $ y =>
           Option.map (fn neq => @{thm neq_to_eq_False} OF [neq])
             (get_fst_success (neq_x_y ctxt x y) names)
-      | _ => NONE),
-    identifier = []};
+      | _ => NONE)};
 
 end;