tuned -- avoid non-standard extend;

--- 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;