src/Pure/consts.ML

--- a/src/Pure/consts.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/consts.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -29,10 +29,9 @@
   val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   val typargs: T -> string * typ -> typ list
   val instance: T -> string * typ list -> typ
-  val declare: Proof.context -> Name_Space.naming -> binding * typ -> T -> T
+  val declare: Context.generic -> binding * typ -> T -> T
   val constrain: string * typ option -> T -> T
-  val abbreviate: Proof.context -> Type.tsig -> Name_Space.naming -> string ->
-    binding * term -> T -> (term * term) * T
+  val abbreviate: Context.generic -> Type.tsig -> string -> binding * term -> T -> (term * term) * T
   val revert_abbrev: string -> string -> T -> T
   val hide: bool -> string -> T -> T
   val empty: T
@@ -232,12 +231,12 @@
 
 (* declarations *)
 
-fun declare ctxt naming (b, declT) =
+fun declare context (b, declT) =
   map_consts (fn (decls, constraints, rev_abbrevs) =>
     let
       val decl = {T = declT, typargs = typargs_of declT};
       val _ = Binding.check b;
-      val (_, decls') = decls |> Name_Space.define ctxt true naming (b, (decl, NONE));
+      val (_, decls') = decls |> Name_Space.define context true (b, (decl, NONE));
     in (decls', constraints, rev_abbrevs) end);
 
 
@@ -268,9 +267,9 @@
 
 in
 
-fun abbreviate ctxt tsig naming mode (b, raw_rhs) consts =
+fun abbreviate context tsig mode (b, raw_rhs) consts =
   let
-    val pp = Context.pretty ctxt;
+    val pp = Context.pretty_generic context;
     val cert_term = certify pp tsig false consts;
     val expand_term = certify pp tsig true consts;
     val force_expand = mode = Print_Mode.internal;
@@ -284,7 +283,7 @@
       |> Term.close_schematic_term;
     val normal_rhs = expand_term rhs;
     val T = Term.fastype_of rhs;
-    val lhs = Const (Name_Space.full_name naming b, T);
+    val lhs = Const (Name_Space.full_name (Name_Space.naming_of context) b, T);
   in
     consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
       let
@@ -292,7 +291,7 @@
         val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
         val _ = Binding.check b;
         val (_, decls') = decls
-          |> Name_Space.define ctxt true naming (b, (decl, SOME abbr));
+          |> Name_Space.define context true (b, (decl, SOME abbr));
         val rev_abbrevs' = rev_abbrevs
           |> update_abbrevs mode (rev_abbrev lhs rhs);
       in (decls', constraints, rev_abbrevs') end)