src/Pure/theory.ML
changeset 74262 839a6e284545
parent 74236 ef74cf118da3
child 74266 612b7e0d6721
--- a/src/Pure/theory.ML	Tue Sep 07 21:16:22 2021 +0200
+++ b/src/Pure/theory.ML	Tue Sep 07 21:47:50 2021 +0200
@@ -125,12 +125,12 @@
 fun init_markup (name, pos) thy =
   let
     val id = serial ();
-    val _ = Context_Position.reports_global thy [(pos, theory_markup true name id pos)];
+    val _ = Context_Position.reports_global thy [(pos, theory_markup {def = true} name id pos)];
   in map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers)) thy end;
 
 fun get_markup thy =
   let val {pos, id, ...} = rep_theory thy
-  in theory_markup false (Context.theory_long_name thy) id pos end;
+  in theory_markup {def = false} (Context.theory_long_name thy) id pos end;
 
 fun check long ctxt (name, pos) =
   let