# HG changeset patch
# User wenzelm
# Date 1595010178 -7200
# Node ID f8d28617ea084fab33c23bfe3eb9a1afff6f1746
# Parent  ce3f26b4e79019a919cc04be9ec5088cb84bcbcb
tuned -- avoid non-standard extend;

diff -r ce3f26b4e790 -r f8d28617ea08 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Jul 17 19:10:24 2020 +0200
+++ b/src/Pure/sign.ML	Fri Jul 17 20:22:58 2020 +0200
@@ -136,10 +136,8 @@
 structure Data = Theory_Data'
 (
   type T = sign;
-  fun extend (Sign {syn, tsig, consts, ...}) = make_sign (syn, tsig, consts);
-
+  val extend = I;
   val empty = make_sign (Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
-
   fun merge old_thys (sign1, sign2) =
     let
       val Sign {syn = syn1, tsig = tsig1, consts = consts1} = sign1;