src/HOL/Statespace/state_space.ML
changeset 42052 34f1d2d81284
parent 41585 45d7da4e4ccf
child 42264 b6c1b0c4c511
     1.1 --- a/src/HOL/Statespace/state_space.ML	Tue Mar 22 14:45:48 2011 +0100
     1.2 +++ b/src/HOL/Statespace/state_space.ML	Tue Mar 22 15:32:47 2011 +0100
     1.3 @@ -623,7 +623,11 @@
     1.4             then Syntax.const "StateFun.lookup" $ Syntax.const "undefined" $ Syntax.free n $ s
     1.5             else raise TERM ("StateSpace.gen_lookup_tr: component " ^ n ^ " not defined",[]));
     1.6  
     1.7 -fun lookup_tr ctxt [s,Free (n,_)] = gen_lookup_tr ctxt s n;
     1.8 +fun lookup_tr ctxt [s, x] =
     1.9 +  (case Syntax.strip_positions x of
    1.10 +    Free (n,_) => gen_lookup_tr ctxt s n
    1.11 +  | _ => raise Match);
    1.12 +
    1.13  fun lookup_swap_tr ctxt [Free (n,_),s] = gen_lookup_tr ctxt s n;
    1.14  
    1.15  fun lookup_tr' ctxt [_$Free (prj,_),n as (_$Free (name,_)),s] =
    1.16 @@ -651,7 +655,10 @@
    1.17           else raise TERM ("StateSpace.gen_update_tr: component " ^ n ^ " not defined",[]))
    1.18     end;
    1.19  
    1.20 -fun update_tr ctxt [s,Free (n,_),v] = gen_update_tr false ctxt n v s;
    1.21 +fun update_tr ctxt [s, x, v] =
    1.22 +  (case Syntax.strip_positions x of
    1.23 +    Free (n, _) => gen_update_tr false ctxt n v s
    1.24 +  | _ => raise Match);
    1.25  
    1.26  fun update_tr' ctxt [_$Free (prj,_),_$Free (inj,_),n as (_$Free (name,_)),(Const (k,_)$v),s] =
    1.27       if Long_Name.base_name k = Long_Name.base_name KN then