src/HOL/Statespace/state_fun.ML
changeset 41472 f6ab14e61604
parent 41227 11e7ee2ca77f
child 42083 e1209fc7ecdc
--- a/src/HOL/Statespace/state_fun.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Statespace/state_fun.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -101,7 +101,7 @@
   val empty = (empty_ss, empty_ss, false);
   val extend = I;
   fun merge ((ss1, ex_ss1, b1), (ss2, ex_ss2, b2)) =
-    (merge_ss (ss1, ss2), merge_ss (ex_ss1, ex_ss2), b1 orelse b2);
+    (merge_ss (ss1, ss2), merge_ss (ex_ss1, ex_ss2), b1 orelse b2 (* FIXME odd merge *));
 );
 
 val init_state_fun_data =