# HG changeset patch
# User wenzelm
# Date 1595010943 -7200
# Node ID 69880fdc8310ff306ca7a98da47ed153cc9cdbd1
# Parent  f8d28617ea084fab33c23bfe3eb9a1afff6f1746
clarified -- avoid non-standard extend/merge;

diff -r f8d28617ea08 -r 69880fdc8310 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Fri Jul 17 20:22:58 2020 +0200
+++ b/src/Pure/theory.ML	Fri Jul 17 20:35:43 2020 +0200
@@ -87,21 +87,18 @@
 structure Thy = Theory_Data'
 (
   type T = thy;
+  val extend = I;
   val empty = make_thy (Position.none, 0, Name_Space.empty_table "axiom", Defs.empty, ([], []));
-
-  fun extend (Thy {pos = _, id = _, axioms, defs, wrappers}) =
-    make_thy (Position.none, 0, axioms, defs, wrappers);
-
   fun merge old_thys (thy1, thy2) =
     let
-      val Thy {pos = _, id = _, axioms = axioms1, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
+      val Thy {pos, id, axioms = axioms1, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
       val Thy {pos = _, id = _, axioms = axioms2, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
 
       val axioms' = Name_Space.merge_tables (axioms1, axioms2);
       val defs' = Defs.merge (Defs.global_context (fst old_thys)) (defs1, defs2);
       val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
       val ens' = Library.merge (eq_snd op =) (ens1, ens2);
-    in make_thy (Position.none, 0, axioms', defs', (bgs', ens')) end;
+    in make_thy (pos, id, axioms', defs', (bgs', ens')) end;
 );
 
 fun rep_theory thy = Thy.get thy |> (fn Thy args => args);