src/HOL/Statespace/state_space.ML

--- a/src/HOL/Statespace/state_space.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Statespace/state_space.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -218,8 +218,7 @@
         Const (@{const_name HOL.eq},_) $ (x as Free _) $ (y as Free _) =>
           Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq])
             (neq_x_y ctxt x y)
-      | _ => NONE),
-    identifier = []};
+      | _ => NONE)};
 
 fun interprete_parent name dist_thm_name parent_expr thy =
   let