src/Pure/Isar/proof_context.ML

--- a/src/Pure/Isar/proof_context.ML	Sun Apr 17 23:47:05 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Apr 18 11:13:29 2011 +0200
@@ -302,7 +302,7 @@
   map_tsig (fn tsig as (local_tsig, global_tsig) =>
     let val thy_tsig = Sign.tsig_of thy in
       if Type.eq_tsig (thy_tsig, global_tsig) then tsig
-      else (Type.merge_tsig (Syntax.pp ctxt) (local_tsig, thy_tsig), thy_tsig)
+      else (Type.merge_tsig (Context.pretty ctxt) (local_tsig, thy_tsig), thy_tsig)
     end) |>
   map_consts (fn consts as (local_consts, global_consts) =>
     let val thy_consts = Sign.consts_of thy in
@@ -376,7 +376,7 @@
 
 fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
   let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
-  in Type.add_arity (Syntax.pp ctxt) arity (tsig_of ctxt); arity end;
+  in Type.add_arity (Context.pretty ctxt) arity (tsig_of ctxt); arity end;
 
 in
 
@@ -546,7 +546,7 @@
 
 local
 
-fun certify_consts ctxt = Consts.certify (Syntax.pp ctxt) (tsig_of ctxt)
+fun certify_consts ctxt = Consts.certify (Context.pretty ctxt) (tsig_of ctxt)
   (not (abbrev_mode ctxt)) (consts_of ctxt);
 
 fun expand_binds ctxt =
@@ -666,9 +666,9 @@
 fun gen_cert prop ctxt t =
   t
   |> expand_abbrevs ctxt
-  |> (fn t' => #1 (Sign.certify' prop (Syntax.pp ctxt) false (consts_of ctxt) (theory_of ctxt) t')
-    handle TYPE (msg, _, _) => error msg
-      | TERM (msg, _) => error msg);
+  |> (fn t' =>
+      #1 (Sign.certify' prop (Context.pretty ctxt) false (consts_of ctxt) (theory_of ctxt) t')
+        handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg);
 
 in