src/Pure/sign.ML

   val restore_naming: theory -> theory -> theory
 end
 
 signature SIGN =
 sig
-  val init_data: theory -> theory
   val rep_sg: theory ->
    {naming: NameSpace.naming,
     syn: Syntax.syntax,
     tsig: Type.tsig,
     consts: Consts.T}

 
 fun make_sign (naming, syn, tsig, consts) =
   Sign {naming = naming, syn = syn, tsig = tsig, consts = consts};
 
 structure SignData = TheoryDataFun
-(struct
-  val name = "Pure/sign";
+(
   type T = sign;
   val copy = I;
   fun extend (Sign {syn, tsig, consts, ...}) =
     make_sign (NameSpace.default_naming, syn, tsig, consts);
 

       val naming = NameSpace.default_naming;
       val syn = Syntax.merge_syntaxes syn1 syn2;
       val tsig = Type.merge_tsigs pp (tsig1, tsig2);
       val consts = Consts.merge (consts1, consts2);
     in make_sign (naming, syn, tsig, consts) end;
-
-  fun print _ _ = ();
-end);
-
-val init_data = SignData.init;
+);
 
 fun rep_sg thy = SignData.get thy |> (fn Sign args => args);
 
 fun map_sign f = SignData.map (fn Sign {naming, syn, tsig, consts} =>
   make_sign (f (naming, syn, tsig, consts)));