src/Pure/sign.ML
changeset 42383 0ae4ad40d7b5
parent 42381 309ec68442c6
child 42387 b1965c8992c8
     1.1 --- a/src/Pure/sign.ML	Sun Apr 17 23:47:05 2011 +0200
     1.2 +++ b/src/Pure/sign.ML	Mon Apr 18 11:13:29 2011 +0200
     1.3 @@ -61,7 +61,7 @@
     1.4    val certify_sort: theory -> sort -> sort
     1.5    val certify_typ: theory -> typ -> typ
     1.6    val certify_typ_mode: Type.mode -> theory -> typ -> typ
     1.7 -  val certify': bool -> Pretty.pp -> bool -> Consts.T -> theory -> term -> term * typ * int
     1.8 +  val certify': bool -> Context.pretty -> bool -> Consts.T -> theory -> term -> term * typ * int
     1.9    val certify_term: theory -> term -> term * typ * int
    1.10    val cert_term: theory -> term -> term
    1.11    val cert_prop: theory -> term -> term
    1.12 @@ -243,7 +243,7 @@
    1.13  (* certify wrt. type signature *)
    1.14  
    1.15  val arity_number = Type.arity_number o tsig_of;
    1.16 -fun arity_sorts thy = Type.arity_sorts (Syntax.pp_global thy) (tsig_of thy);
    1.17 +fun arity_sorts thy = Type.arity_sorts (Context.pretty_global thy) (tsig_of thy);
    1.18  
    1.19  val certify_class         = Type.cert_class o tsig_of;
    1.20  val certify_sort          = Type.cert_sort o tsig_of;
    1.21 @@ -262,7 +262,7 @@
    1.22          val xs = map Free bs;           (*we do not rename here*)
    1.23          val t' = subst_bounds (xs, t);
    1.24          val u' = subst_bounds (xs, u);
    1.25 -        val msg = Type.appl_error pp t' T u' U;
    1.26 +        val msg = Type.appl_error (Syntax.init_pretty pp) t' T u' U;
    1.27        in raise TYPE (msg, [T, U], [t', u']) end;
    1.28  
    1.29      fun typ_of (_, Const (_, T)) = T
    1.30 @@ -301,10 +301,11 @@
    1.31      val tm'' = Consts.certify pp (tsig_of thy) do_expand consts tm';
    1.32    in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end;
    1.33  
    1.34 -fun certify_term thy = certify' false (Syntax.pp_global thy) true (consts_of thy) thy;
    1.35 -fun cert_term_abbrev thy = #1 o certify' false (Syntax.pp_global thy) false (consts_of thy) thy;
    1.36 +fun certify_term thy = certify' false (Context.pretty_global thy) true (consts_of thy) thy;
    1.37 +fun cert_term_abbrev thy =
    1.38 +  #1 o certify' false (Context.pretty_global thy) false (consts_of thy) thy;
    1.39  val cert_term = #1 oo certify_term;
    1.40 -fun cert_prop thy = #1 o certify' true (Syntax.pp_global thy) true (consts_of thy) thy;
    1.41 +fun cert_prop thy = #1 o certify' true (Context.pretty_global thy) true (consts_of thy) thy;
    1.42  
    1.43  end;
    1.44  
    1.45 @@ -457,12 +458,12 @@
    1.46    thy |> map_sign (fn (naming, syn, tsig, consts) =>
    1.47      let
    1.48        val ctxt = Syntax.init_pretty_global thy;
    1.49 -      val tsig' = Type.add_class ctxt (Syntax.pp ctxt) naming (bclass, classes) tsig;
    1.50 +      val tsig' = Type.add_class ctxt (Context.pretty ctxt) naming (bclass, classes) tsig;
    1.51      in (naming, syn, tsig', consts) end)
    1.52    |> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
    1.53  
    1.54 -fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (Syntax.pp_global thy) arg);
    1.55 -fun primitive_arity arg thy = thy |> map_tsig (Type.add_arity (Syntax.pp_global thy) arg);
    1.56 +fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (Context.pretty_global thy) arg);
    1.57 +fun primitive_arity arg thy = thy |> map_tsig (Type.add_arity (Context.pretty_global thy) arg);
    1.58  
    1.59  
    1.60  (* add translation functions *)