src/HOL/Statespace/state_space.ML
changeset 30364 577edc39b501
parent 30346 90efbb8a8cb2
child 30473 e0b66c11e7e4
     1.1 --- a/src/HOL/Statespace/state_space.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/HOL/Statespace/state_space.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -645,7 +645,7 @@
     1.4  fun update_tr ctxt [s,Free (n,_),v] = gen_update_tr false ctxt n v s;
     1.5  
     1.6  fun update_tr' ctxt [_$Free (prj,_),_$Free (inj,_),n as (_$Free (name,_)),(Const (k,_)$v),s] =
     1.7 -     if NameSpace.base_name k = NameSpace.base_name KN then
     1.8 +     if Long_Name.base_name k = Long_Name.base_name KN then
     1.9          (case get_comp (Context.Proof ctxt) name of
    1.10            SOME (T,_) => if inj=inject_name T andalso prj=project_name T then
    1.11                             Syntax.const "_statespace_update" $ s $ n $ v