--- a/src/HOL/Statespace/state_space.ML Sun Mar 08 17:19:15 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML Sun Mar 08 17:26:14 2009 +0100
@@ -645,7 +645,7 @@
fun update_tr ctxt [s,Free (n,_),v] = gen_update_tr false ctxt n v s;
fun update_tr' ctxt [_$Free (prj,_),_$Free (inj,_),n as (_$Free (name,_)),(Const (k,_)$v),s] =
- if NameSpace.base_name k = NameSpace.base_name KN then
+ if Long_Name.base_name k = Long_Name.base_name KN then
(case get_comp (Context.Proof ctxt) name of
SOME (T,_) => if inj=inject_name T andalso prj=project_name T then
Syntax.const "_statespace_update" $ s $ n $ v