src/HOL/Statespace/state_fun.ML
changeset 30364 577edc39b501
parent 30289 b28caca9157f
child 30528 7173bf123335
     1.1 --- a/src/HOL/Statespace/state_fun.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/HOL/Statespace/state_fun.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -336,17 +336,17 @@
     1.4      [] => ""
     1.5     | c::cs => String.implode (Char.toUpper c::cs ))
     1.6  
     1.7 -fun mkName (Type (T,args)) = concat (map mkName args) ^ mkUpper (NameSpace.base_name T)
     1.8 -  | mkName (TFree (x,_)) = mkUpper (NameSpace.base_name x)
     1.9 -  | mkName (TVar ((x,_),_)) = mkUpper (NameSpace.base_name x);
    1.10 +fun mkName (Type (T,args)) = concat (map mkName args) ^ mkUpper (Long_Name.base_name T)
    1.11 +  | mkName (TFree (x,_)) = mkUpper (Long_Name.base_name x)
    1.12 +  | mkName (TVar ((x,_),_)) = mkUpper (Long_Name.base_name x);
    1.13  
    1.14  fun is_datatype thy n = is_some (Symtab.lookup (DatatypePackage.get_datatypes thy) n);
    1.15  
    1.16  fun mk_map "List.list" = Syntax.const "List.map"
    1.17 -  | mk_map n = Syntax.const ("StateFun.map_" ^ NameSpace.base_name n);
    1.18 +  | mk_map n = Syntax.const ("StateFun.map_" ^ Long_Name.base_name n);
    1.19  
    1.20  fun gen_constr_destr comp prfx thy (Type (T,[])) = 
    1.21 -      Syntax.const (deco prfx (mkUpper (NameSpace.base_name T)))
    1.22 +      Syntax.const (deco prfx (mkUpper (Long_Name.base_name T)))
    1.23    | gen_constr_destr comp prfx thy (T as Type ("fun",_)) =
    1.24       let val (argTs,rangeT) = strip_type T;
    1.25       in comp 
    1.26 @@ -360,11 +360,11 @@
    1.27       then (* datatype args are recursively embedded into val *)
    1.28           (case argTs of
    1.29             [argT] => comp 
    1.30 -                     ((Syntax.const (deco prfx (mkUpper (NameSpace.base_name T)))))
    1.31 +                     ((Syntax.const (deco prfx (mkUpper (Long_Name.base_name T)))))
    1.32                       ((mk_map T $ gen_constr_destr comp prfx thy argT))
    1.33            | _ => raise (TYPE ("StateFun.gen_constr_destr",[T'],[])))
    1.34       else (* type args are not recursively embedded into val *)
    1.35 -           Syntax.const (deco prfx (concat (map mkName argTs) ^ mkUpper (NameSpace.base_name T)))
    1.36 +           Syntax.const (deco prfx (concat (map mkName argTs) ^ mkUpper (Long_Name.base_name T)))
    1.37    | gen_constr_destr thy _ _ T = raise (TYPE ("StateFun.gen_constr_destr",[T],[]));
    1.38                     
    1.39  val mk_constr = gen_constr_destr (fn a => fn b => Syntax.const "Fun.comp" $ a $ b) ""