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 =