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/Isar/class_declaration.ML
changeset 81116 0fb1e2dd4122
parent 79438 032ca41f590a 
--- a/src/Pure/Isar/class_declaration.ML	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Sat Oct 05 14:58:36 2024 +0200
@@ -8,7 +8,7 @@
 sig
   val class: binding -> Bundle.name list -> class list ->
     Element.context_i list -> theory -> string * local_theory
-  val class_cmd: binding -> (xstring * Position.T) list -> xstring list ->
+  val class_cmd: binding -> Bundle.xname list -> xstring list ->
     Element.context list -> theory -> string * local_theory
   val prove_subclass: tactic -> class ->
     local_theory -> local_theory
@@ -263,7 +263,7 @@
   in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (includes, elems, global_syntax)) end;
 
 val cert_class_spec = prep_class_spec (K I) (K I) cert_class_elems;
-val read_class_spec = prep_class_spec Proof_Context.read_class Bundle.check read_class_elems;
+val read_class_spec = prep_class_spec Proof_Context.read_class Bundle.check_name read_class_elems;
 
 
 (* class establishment *)
isabelle