Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/thm_name.ML
changeset 81535 db073d1733ab
parent 80590 505f97165f52 
--- a/src/Pure/thm_name.ML	Mon Dec 02 11:22:44 2024 +0100
+++ b/src/Pure/thm_name.ML	Mon Dec 02 11:36:53 2024 +0100
@@ -23,7 +23,7 @@
   val expr: string * Position.T -> ('a list * 'b) list -> ((P * 'a) list * 'b) list
 
   val parse: string -> T
-  val print_prefix: Context.generic -> Name_Space.T -> T -> Markup.T * string
+  val print_prefix: Proof.context -> Name_Space.T -> T -> Markup.T * string
   val print_suffix: T -> string
   val print: T -> string
   val print_pos: P -> string
@@ -99,9 +99,9 @@
 
 (* print *)
 
-fun print_prefix context space ((name, _): T) =
+fun print_prefix ctxt space ((name, _): T) =
   if name = "" then (Markup.empty, "")
-  else (Name_Space.markup space name, Name_Space.extern_generic context space name);
+  else (Name_Space.markup space name, Name_Space.extern ctxt space name);
 
 fun print_suffix (name, index) =
   if name = "" orelse index = 0 then ""
isabelle