src/Pure/axclass.ML
changeset 39133 70d3915c92f0
parent 38383 1ad96229b455
child 39134 917b4b6ba3d2
     1.1 --- a/src/Pure/axclass.ML	Sat Sep 04 22:36:42 2010 +0200
     1.2 +++ b/src/Pure/axclass.ML	Sun Sep 05 19:47:40 2010 +0200
     1.3 @@ -507,8 +507,7 @@
     1.4  
     1.5  fun define_class (bclass, raw_super) raw_params raw_specs thy =
     1.6    let
     1.7 -    val ctxt = ProofContext.init_global thy;
     1.8 -    val pp = Syntax.pp ctxt;
     1.9 +    val ctxt = Syntax.init_pretty_global thy;
    1.10  
    1.11  
    1.12      (* class *)
    1.13 @@ -520,8 +519,8 @@
    1.14      fun check_constraint (a, S) =
    1.15        if Sign.subsort thy (super, S) then ()
    1.16        else error ("Sort constraint of type variable " ^
    1.17 -        setmp_CRITICAL show_sorts true (Pretty.string_of_typ pp) (TFree (a, S)) ^
    1.18 -        " needs to be weaker than " ^ Pretty.string_of_sort pp super);
    1.19 +        setmp_CRITICAL show_sorts true (Syntax.string_of_typ ctxt) (TFree (a, S)) ^
    1.20 +        " needs to be weaker than " ^ Syntax.string_of_sort ctxt super);
    1.21  
    1.22  
    1.23      (* params *)
    1.24 @@ -543,7 +542,7 @@
    1.25        (case Term.add_tfrees t [] of
    1.26          [(a, S)] => check_constraint (a, S)
    1.27        | [] => ()
    1.28 -      | _ => error ("Multiple type variables in class axiom:\n" ^ Pretty.string_of_term pp t);
    1.29 +      | _ => error ("Multiple type variables in class axiom:\n" ^ Syntax.string_of_term ctxt t);
    1.30        t
    1.31        |> Term.map_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U))
    1.32        |> Logic.close_form);
    1.33 @@ -590,7 +589,7 @@
    1.34        |> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> #2
    1.35        |> Sign.restore_naming facts_thy
    1.36        |> map_axclasses (Symtab.update (class, axclass))
    1.37 -      |> map_params (fold (fn (x, _) => add_param pp (x, class)) params);
    1.38 +      |> map_params (fold (fn (x, _) => add_param (Syntax.pp ctxt) (x, class)) params);
    1.39  
    1.40    in (class, result_thy) end;
    1.41