src/Pure/axclass.ML
changeset 26939 1035c89b4c02
parent 26516 1bf210ac0a90
child 27397 1d8456c5d53d
     1.1 --- a/src/Pure/axclass.ML	Sat May 17 23:53:20 2008 +0200
     1.2 +++ b/src/Pure/axclass.ML	Sun May 18 15:04:09 2008 +0200
     1.3 @@ -224,13 +224,14 @@
     1.4  
     1.5  fun cert_classrel thy raw_rel =
     1.6    let
     1.7 +    val string_of_sort = Syntax.string_of_sort_global thy;
     1.8      val (c1, c2) = pairself (Sign.certify_class thy) raw_rel;
     1.9      val _ = Sign.primitive_classrel (c1, c2) (Theory.copy thy);
    1.10      val _ =
    1.11        (case subtract (op =) (all_params_of thy [c1]) (all_params_of thy [c2]) of
    1.12          [] => ()
    1.13 -      | xs => raise TYPE ("Class " ^ Sign.string_of_sort thy [c1] ^ " lacks parameter(s) " ^
    1.14 -          commas_quote xs ^ " of " ^ Sign.string_of_sort thy [c2], [], []));
    1.15 +      | xs => raise TYPE ("Class " ^ string_of_sort [c1] ^ " lacks parameter(s) " ^
    1.16 +          commas_quote xs ^ " of " ^ string_of_sort [c2], [], []));
    1.17    in (c1, c2) end;
    1.18  
    1.19  fun read_classrel thy raw_rel =
    1.20 @@ -314,7 +315,7 @@
    1.21      val tyco = case inst_tyco_of thy (c, T)
    1.22       of SOME tyco => tyco
    1.23        | NONE => error ("Illegal type for instantiation of class parameter: "
    1.24 -        ^ quote (c ^ " :: " ^ Sign.string_of_typ thy T));
    1.25 +        ^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T));
    1.26      val name_inst = instance_name (tyco, class) ^ "_inst";
    1.27      val c' = NameSpace.base c ^ "_" ^ NameSpace.base tyco;
    1.28      val T' = Type.strip_sorts T;
    1.29 @@ -518,7 +519,8 @@
    1.30                | _ => I) typ [];
    1.31          val hyps = vars
    1.32            |> map (fn (T, S) => (T, Drule.sort_triv thy (T, S) ~~ S));
    1.33 -        val ths = (typ, sort) |> Sorts.of_sort_derivation (Sign.pp thy) (Sign.classes_of thy)
    1.34 +        val ths = (typ, sort)
    1.35 +          |> Sorts.of_sort_derivation (Syntax.pp_global thy) (Sign.classes_of thy)
    1.36             {class_relation =
    1.37                fn (th, c1) => fn c2 => th RS the_classrel thy (c1, c2),
    1.38              type_constructor =
    1.39 @@ -536,7 +538,7 @@
    1.40      val sort' = filter (is_none o lookup_type cache typ) sort;
    1.41      val ths' = derive_type thy (typ, sort')
    1.42        handle ERROR msg => cat_error msg ("The error(s) above occurred for sort derivation: " ^
    1.43 -        Sign.string_of_typ thy typ ^ " :: " ^ Sign.string_of_sort thy sort');
    1.44 +        Syntax.string_of_typ_global thy typ ^ " :: " ^ Syntax.string_of_sort_global thy sort');
    1.45      val cache' = cache |> fold (insert_type typ) (sort' ~~ ths');
    1.46      val ths =
    1.47        sort |> map (fn c =>