src/Pure/Isar/class_target.ML
changeset 30364 577edc39b501
parent 30344 10a67c5ddddb
child 30510 4120fc59dd85
child 30519 c05c0199826f
     1.1 --- a/src/Pure/Isar/class_target.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/Pure/Isar/class_target.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -300,7 +300,7 @@
     1.4    map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) o these_operations thy;
     1.5  
     1.6  fun redeclare_const thy c =
     1.7 -  let val b = NameSpace.base_name c
     1.8 +  let val b = Long_Name.base_name c
     1.9    in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end;
    1.10  
    1.11  fun synchronize_class_syntax sort base_sort ctxt =
    1.12 @@ -358,7 +358,7 @@
    1.13  
    1.14  (* class target *)
    1.15  
    1.16 -val class_prefix = Logic.const_of_class o NameSpace.base_name;
    1.17 +val class_prefix = Logic.const_of_class o Long_Name.base_name;
    1.18  
    1.19  fun declare class pos ((c, mx), dict) thy =
    1.20    let
    1.21 @@ -475,7 +475,7 @@
    1.22  
    1.23  fun type_name "*" = "prod"
    1.24    | type_name "+" = "sum"
    1.25 -  | type_name s = sanatize_name (NameSpace.base_name s);
    1.26 +  | type_name s = sanatize_name (Long_Name.base_name s);
    1.27  
    1.28  fun resort_terms pp algebra consts constraints ts =
    1.29    let