src/HOL/Statespace/state_space.ML

     val parent_comps =
       maps (fn (Ts',n,rs) => parent_components thy (map subst Ts',n,rs)) parents;
     val all_comps = rename renaming (parent_comps @ map (apsnd subst) components);
   in all_comps end;
 
-fun take_upto i xs = List.take(xs,i) handle Subscript => xs;
+fun take_upto i xs = List.take(xs,i) handle General.Subscript => xs;
 
 fun statespace_definition state_type args name parents parent_comps components thy =
   let
     val full_name = Sign.full_bname thy name;
     val all_comps = parent_comps @ components;