--- a/src/Pure/consts.ML Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/consts.ML Fri Sep 25 19:13:47 2015 +0200
@@ -27,7 +27,7 @@
val intern: T -> xstring -> string
val intern_syntax: T -> xstring -> string
val check_const: Context.generic -> T -> xstring * Position.T list -> term * Position.report list
- val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*)
+ val certify: Context.generic -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*)
val typargs: T -> string * typ -> typ list
val instance: T -> string * typ list -> typ
val declare: Context.generic -> binding * typ -> T -> T
@@ -155,11 +155,11 @@
(* certify *)
-fun certify pp tsig do_expand consts =
+fun certify context tsig do_expand consts =
let
fun err msg (c, T) =
raise TYPE (msg ^ " " ^ quote c ^ " :: " ^
- Syntax.string_of_typ (Syntax.init_pretty pp) T, [], []);
+ Syntax.string_of_typ (Syntax.init_pretty context) T, [], []);
val certT = Type.cert_typ tsig;
fun cert tm =
let
@@ -272,9 +272,8 @@
fun abbreviate context tsig mode (b, raw_rhs) consts =
let
- val pp = Context.pretty_generic context;
- val cert_term = certify pp tsig false consts;
- val expand_term = certify pp tsig true consts;
+ val cert_term = certify context tsig false consts;
+ val expand_term = certify context tsig true consts;
val force_expand = mode = Print_Mode.internal;
val _ = Term.exists_subterm Term.is_Var raw_rhs andalso