sg_ref: automatic adjustment of thms of draft theories;
authorwenzelm
Tue Oct 21 18:09:13 1997 +0200 (1997-10-21)
changeset 3967edd5ff9371f8
parent 3966 b06face07498
child 3968 ec138de716d9
sg_ref: automatic adjustment of thms of draft theories;
src/Pure/sign.ML
src/Pure/theory.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/sign.ML	Tue Oct 21 17:48:06 1997 +0200
     1.2 +++ b/src/Pure/sign.ML	Tue Oct 21 18:09:13 1997 +0200
     1.3 @@ -18,14 +18,20 @@
     1.4  signature SIGN =
     1.5  sig
     1.6    type sg
     1.7 +  type sg_ref
     1.8    val rep_sg: sg ->
     1.9 -   {tsig: Type.type_sig,
    1.10 +   {id: string ref,			(* FIXME hide!? *)
    1.11 +    self: sg_ref,
    1.12 +    tsig: Type.type_sig,
    1.13      const_tab: typ Symtab.table,
    1.14      syn: Syntax.syntax,
    1.15      path: string list,
    1.16      spaces: (string * NameSpace.T) list,
    1.17      data: Data.T,
    1.18 -    stamps: string ref list}
    1.19 +    stamps: string ref list}		(* FIXME hide!? *)
    1.20 +  val tsig_of: sg -> Type.type_sig
    1.21 +  val deref: sg_ref -> sg
    1.22 +  val self_ref: sg -> sg_ref
    1.23    val subsig: sg * sg -> bool
    1.24    val eq_sg: sg * sg -> bool
    1.25    val same_sg: sg * sg -> bool
    1.26 @@ -108,9 +114,9 @@
    1.27    val get_data: sg -> string -> exn
    1.28    val put_data: string * exn -> sg -> sg
    1.29    val print_data: sg -> string -> unit
    1.30 -  val prep_ext: sg -> sg
    1.31 +  val merge_refs: sg_ref * sg_ref -> sg_ref
    1.32 +  val make_draft: sg -> sg
    1.33    val merge: sg * sg -> sg
    1.34 -  val nontriv_merge: sg * sg -> sg
    1.35    val proto_pure: sg
    1.36    val pure: sg
    1.37    val cpure: sg
    1.38 @@ -121,22 +127,55 @@
    1.39  structure Sign : SIGN =
    1.40  struct
    1.41  
    1.42 +
    1.43  (** datatype sg **)
    1.44  
    1.45  datatype sg =
    1.46    Sg of {
    1.47 +    id: string ref,				(*id*)
    1.48 +    self: sg_ref,				(*mutable self reference*)
    1.49      tsig: Type.type_sig,                        (*order-sorted signature of types*)
    1.50      const_tab: typ Symtab.table,                (*type schemes of constants*)
    1.51      syn: Syntax.syntax,                         (*syntax for parsing and printing*)
    1.52      path: string list,                     	(*current name space entry prefix*)
    1.53      spaces: (string * NameSpace.T) list,   	(*name spaces for consts, types etc.*)
    1.54      data: Data.T,				(*additional data*)
    1.55 -    stamps: string ref list};                   (*unique theory indentifier*)
    1.56 +    stamps: string ref list}                    (*unique theory indentifier*)
    1.57        (*the "ref" in stamps ensures that no two signatures are identical
    1.58          -- it is impossible to forge a signature*)
    1.59 +and sg_ref =
    1.60 +  SgRef of sg ref option;
    1.61  
    1.62 +(*make signature*)
    1.63 +fun make_sign (id, self, tsig, const_tab, syn, path, spaces, data, stamps) =
    1.64 +  Sg {id = id, self = self, tsig = tsig, const_tab = const_tab, syn = syn,
    1.65 +    path = path, spaces = spaces, data = data, stamps = stamps};
    1.66 +
    1.67 +(*dest signature*)
    1.68  fun rep_sg (Sg args) = args;
    1.69  val tsig_of = #tsig o rep_sg;
    1.70 +val self_ref = #self o rep_sg;
    1.71 +
    1.72 +fun get_data (Sg {data, ...}) = Data.get data;
    1.73 +fun print_data (Sg {data, ...}) = Data.print data;
    1.74 +
    1.75 +
    1.76 +(*show stamps*)
    1.77 +fun stamp_names stamps = rev (map ! stamps);
    1.78 +
    1.79 +fun pretty_sg (Sg {stamps, ...}) = Pretty.str_list "{" "}" (stamp_names stamps);
    1.80 +val pprint_sg = Pretty.pprint o pretty_sg;
    1.81 +
    1.82 +
    1.83 +(* signature id *)
    1.84 +
    1.85 +fun deref (SgRef (Some (ref sg))) = sg
    1.86 +  | deref (SgRef None) = sys_error "Sign.deref";
    1.87 +
    1.88 +fun check_stale (sg as Sg {id, self = SgRef (Some (ref (Sg {id = id', ...}))), ...}) =
    1.89 +      if id = id' then sg
    1.90 +      else raise TERM ("Stale signature: " ^ Pretty.str_of (pretty_sg sg), [])
    1.91 +  | check_stale _ = sys_error "Sign.check_stale";
    1.92  
    1.93  
    1.94  (* inclusion and equality *)
    1.95 @@ -157,28 +196,62 @@
    1.96          if x = y then fast_sub (xs, ys)
    1.97          else fast_sub (x :: xs, ys);
    1.98  in
    1.99 -  fun subsig (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
   1.100 -    s1 = s2 orelse subset_stamp (s1, s2);
   1.101 +  fun eq_sg (sg1 as Sg {id = id1, ...}, sg2 as Sg {id = id2, ...}) =
   1.102 +    (check_stale sg1; check_stale sg2; id1 = id2);
   1.103  
   1.104 -  fun fast_subsig (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
   1.105 -    s1 = s2 orelse fast_sub (s1, s2);
   1.106 +  fun subsig (sg1 as Sg {stamps = s1, ...}, sg2 as Sg {stamps = s2, ...}) =
   1.107 +    eq_sg (sg1, sg2) orelse subset_stamp (s1, s2);
   1.108  
   1.109 -  fun eq_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
   1.110 -    s1 = s2 orelse (subset_stamp (s1, s2) andalso subset_stamp (s2, s1));
   1.111 +  fun fast_subsig (sg1 as Sg {stamps = s1, ...}, sg2 as Sg {stamps = s2, ...}) =
   1.112 +    eq_sg (sg1, sg2) orelse fast_sub (s1, s2);
   1.113  end;
   1.114  
   1.115  
   1.116  (*test if same theory names are contained in signatures' stamps,
   1.117    i.e. if signatures belong to same theory but not necessarily to the
   1.118    same version of it*)
   1.119 -fun same_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
   1.120 -  eq_set_string (pairself (map (op !)) (s1, s2));
   1.121 +fun same_sg (sg1 as Sg {stamps = s1, ...}, sg2 as Sg {stamps = s2, ...}) =
   1.122 +  eq_sg (sg1, sg2) orelse eq_set_string (pairself (map (op !)) (s1, s2));
   1.123  
   1.124  (*test for drafts*)
   1.125  fun is_draft (Sg {stamps = ref "#" :: _, ...}) = true
   1.126    | is_draft _ = false;
   1.127  
   1.128  
   1.129 +(* build signature *)
   1.130 +
   1.131 +fun ext_stamps stamps (id as ref name) =
   1.132 +  let val stmps = (case stamps of ref "#" :: ss => ss | ss => ss) in
   1.133 +    if exists (equal name o !) stmps then
   1.134 +      error ("Theory already contains a " ^ quote name ^ " component")
   1.135 +    else id :: stmps
   1.136 +  end;
   1.137 +
   1.138 +fun create_sign self stamps name (syn, tsig, ctab, (path, spaces), data) =
   1.139 +  let
   1.140 +    val id = ref name;
   1.141 +    val sign =
   1.142 +      make_sign (id, self, tsig, ctab, syn, path, spaces, data, ext_stamps stamps id);
   1.143 +  in
   1.144 +    (case self of
   1.145 +      SgRef (Some r) => r := sign
   1.146 +    | _ => sys_error "Sign.create_sign");
   1.147 +    sign
   1.148 +  end;
   1.149 +
   1.150 +fun extend_sign extfun name decls
   1.151 +    (sg as Sg {id = _, self, tsig, const_tab, syn, path, spaces, data, stamps}) =
   1.152 +  let
   1.153 +    val _ = check_stale sg;
   1.154 +    val (self', data') =
   1.155 +      if is_draft sg then (self, data)
   1.156 +      else (SgRef (Some (ref sg)), Data.prep_ext data);
   1.157 +  in
   1.158 +    create_sign self' stamps name
   1.159 +      (extfun (syn, tsig, const_tab, (path, spaces), data') decls)
   1.160 +  end;
   1.161 +
   1.162 +
   1.163  (* consts *)
   1.164  
   1.165  fun const_type (Sg {const_tab, ...}) c = Symtab.lookup (const_tab, c);
   1.166 @@ -320,6 +393,7 @@
   1.167    val intern_tycons = intrn_tycons o spaces_of;
   1.168  
   1.169    fun full_name (Sg {path, ...}) = full path;
   1.170 +
   1.171  end;
   1.172  
   1.173  
   1.174 @@ -368,8 +442,6 @@
   1.175  
   1.176  (** print signature **)
   1.177  
   1.178 -fun stamp_names stamps = rev (map ! stamps);
   1.179 -
   1.180  fun print_sg sg =
   1.181    let
   1.182      fun prt_cls c = pretty_sort sg [c];
   1.183 @@ -405,7 +477,7 @@
   1.184      fun pretty_const (c, ty) = Pretty.block
   1.185        [prt_const c, Pretty.str " ::", Pretty.brk 1, prt_typ ty];
   1.186  
   1.187 -    val Sg {tsig, const_tab, syn = _, path, spaces, data, stamps} = sg;
   1.188 +    val Sg {id = _, self = _, tsig, const_tab, syn = _, path, spaces, data, stamps} = sg;
   1.189      val spaces' = sort (fn ((k1, _), (k2, _)) => k1 < k2) spaces;
   1.190      val {classes, classrel, default, tycons, abbrs, arities} =
   1.191        Type.rep_tsig tsig;
   1.192 @@ -424,12 +496,6 @@
   1.193    end;
   1.194  
   1.195  
   1.196 -fun pretty_sg (Sg {stamps, ...}) =
   1.197 -  Pretty.str_list "{" "}" (stamp_names stamps);
   1.198 -
   1.199 -val pprint_sg = Pretty.pprint o pretty_sg;
   1.200 -
   1.201 -
   1.202  
   1.203  (** read types **)  (*exception ERROR*)
   1.204  
   1.205 @@ -598,18 +664,18 @@
   1.206  
   1.207  (* add default sort *)
   1.208  
   1.209 -fun ext_defsort int (syn, tsig, ctab, (path, spaces)) S =
   1.210 +fun ext_defsort int (syn, tsig, ctab, (path, spaces), data) S =
   1.211    (syn, Type.ext_tsig_defsort tsig (if int then intrn_sort spaces S else S),
   1.212 -    ctab, (path, spaces));
   1.213 +    ctab, (path, spaces), data);
   1.214  
   1.215  
   1.216  (* add type constructors *)
   1.217  
   1.218 -fun ext_types (syn, tsig, ctab, (path, spaces)) types =
   1.219 +fun ext_types (syn, tsig, ctab, (path, spaces), data) types =
   1.220    let val decls = decls_of path Syntax.type_name types in
   1.221      (Syntax.extend_type_gram syn types,
   1.222        Type.ext_tsig_types tsig decls, ctab,
   1.223 -      (path, add_names spaces typeK (map fst decls)))
   1.224 +      (path, add_names spaces typeK (map fst decls)), data)
   1.225    end;
   1.226  
   1.227  
   1.228 @@ -619,7 +685,7 @@
   1.229    (t, vs, read_raw_typ syn tsig spaces (K None) rhs_src)
   1.230      handle ERROR => error ("in type abbreviation " ^ t);
   1.231  
   1.232 -fun ext_abbrs rd_abbr (syn, tsig, ctab, (path, spaces)) abbrs =
   1.233 +fun ext_abbrs rd_abbr (syn, tsig, ctab, (path, spaces), data) abbrs =
   1.234    let
   1.235      fun mfix_of (t, vs, _, mx) = (t, length vs, mx);
   1.236      val syn' = Syntax.extend_type_gram syn (map mfix_of abbrs);
   1.237 @@ -630,7 +696,7 @@
   1.238      val spaces' = add_names spaces typeK (map #1 abbrs');
   1.239      val decls = map (rd_abbr syn' tsig spaces') abbrs';
   1.240    in
   1.241 -    (syn', Type.ext_tsig_abbrs tsig decls, ctab, (path, spaces'))
   1.242 +    (syn', Type.ext_tsig_abbrs tsig decls, ctab, (path, spaces'), data)
   1.243    end;
   1.244  
   1.245  fun ext_tyabbrs abbrs = ext_abbrs read_abbr abbrs;
   1.246 @@ -639,7 +705,7 @@
   1.247  
   1.248  (* add type arities *)
   1.249  
   1.250 -fun ext_arities int (syn, tsig, ctab, (path, spaces)) arities =
   1.251 +fun ext_arities int (syn, tsig, ctab, (path, spaces), data) arities =
   1.252    let
   1.253      fun intrn_arity (c, Ss, S) =
   1.254        (intrn spaces typeK c, map (intrn_sort spaces) Ss, intrn_sort spaces S);
   1.255 @@ -647,7 +713,7 @@
   1.256      val tsig' = Type.ext_tsig_arities tsig (intrn arities);
   1.257      val log_types = Type.logical_types tsig';
   1.258    in
   1.259 -    (Syntax.extend_log_types syn log_types, tsig', ctab, (path, spaces))
   1.260 +    (Syntax.extend_log_types syn log_types, tsig', ctab, (path, spaces), data)
   1.261    end;
   1.262  
   1.263  
   1.264 @@ -667,7 +733,7 @@
   1.265    (c, read_raw_typ syn tsig spaces (K None) ty_src, mx)
   1.266      handle ERROR => err_in_const (const_name path c mx);
   1.267  
   1.268 -fun ext_cnsts rd_const syn_only prmode (syn, tsig, ctab, (path, spaces)) raw_consts =
   1.269 +fun ext_cnsts rd_const syn_only prmode (syn, tsig, ctab, (path, spaces), data) raw_consts =
   1.270    let
   1.271      fun prep_const (c, ty, mx) =
   1.272        (c, compress_type (Type.varifyT (Type.cert_typ tsig (Type.no_tvars ty))), mx)
   1.273 @@ -682,7 +748,7 @@
   1.274      (Syntax.extend_const_gram syn prmode consts, tsig,
   1.275        Symtab.extend_new (ctab, decls)
   1.276          handle Symtab.DUPS cs => err_dup_consts cs,
   1.277 -      (path, add_names spaces constK (map fst decls)))
   1.278 +      (path, add_names spaces constK (map fst decls)), data)
   1.279    end;
   1.280  
   1.281  val ext_consts_i = ext_cnsts no_read false ("", true);
   1.282 @@ -706,7 +772,7 @@
   1.283    end;
   1.284  
   1.285  
   1.286 -fun ext_classes int (syn, tsig, ctab, (path, spaces)) classes =
   1.287 +fun ext_classes int (syn, tsig, ctab, (path, spaces), data) classes =
   1.288    let
   1.289      val names = map fst classes;
   1.290      val consts =
   1.291 @@ -720,62 +786,51 @@
   1.292    in
   1.293      ext_consts_i
   1.294        (Syntax.extend_consts syn names,
   1.295 -        Type.ext_tsig_classes tsig classes', ctab, (path, spaces'))
   1.296 +        Type.ext_tsig_classes tsig classes', ctab, (path, spaces'), data)
   1.297      consts
   1.298    end;
   1.299  
   1.300  
   1.301  (* add to classrel *)
   1.302  
   1.303 -fun ext_classrel int (syn, tsig, ctab, (path, spaces)) pairs =
   1.304 +fun ext_classrel int (syn, tsig, ctab, (path, spaces), data) pairs =
   1.305    let val intrn = if int then map (pairself (intrn_class spaces)) else I in
   1.306 -    (syn, Type.ext_tsig_classrel tsig (intrn pairs), ctab, (path, spaces))
   1.307 +    (syn, Type.ext_tsig_classrel tsig (intrn pairs), ctab, (path, spaces), data)
   1.308    end;
   1.309  
   1.310  
   1.311  (* add to syntax *)
   1.312  
   1.313 -fun ext_syn extfun (syn, tsig, ctab, names) args =
   1.314 -  (extfun syn args, tsig, ctab, names);
   1.315 +fun ext_syn extfun (syn, tsig, ctab, names, data) args =
   1.316 +  (extfun syn args, tsig, ctab, names, data);
   1.317  
   1.318  
   1.319  (* add to path *)
   1.320  
   1.321 -fun ext_path (syn, tsig, ctab, (path, spaces)) elem =
   1.322 +fun ext_path (syn, tsig, ctab, (path, spaces), data) elem =
   1.323    let
   1.324      val path' =
   1.325        if elem = ".." andalso not (null path) then fst (split_last path)
   1.326        else if elem = "/" then []
   1.327        else path @ NameSpace.unpack elem;
   1.328    in
   1.329 -    (syn, tsig, ctab, (path', spaces))
   1.330 +    (syn, tsig, ctab, (path', spaces), data)
   1.331    end;      
   1.332  
   1.333  
   1.334  (* add to name space *)
   1.335  
   1.336 -fun ext_space (syn, tsig, ctab, (path, spaces)) (kind, names) =
   1.337 -  (syn, tsig, ctab, (path, add_names spaces kind names));
   1.338 +fun ext_space (syn, tsig, ctab, (path, spaces), data) (kind, names) =
   1.339 +  (syn, tsig, ctab, (path, add_names spaces kind names), data);
   1.340  
   1.341  
   1.342 -(* build signature *)
   1.343 +(* signature data *)
   1.344  
   1.345 -fun ext_stamps stamps name =
   1.346 -  let
   1.347 -    val stmps = (case stamps of ref "#" :: ss => ss | ss => ss);
   1.348 -  in
   1.349 -    if exists (equal name o !) stmps then
   1.350 -      error ("Theory already contains a " ^ quote name ^ " component")
   1.351 -    else ref name :: stmps
   1.352 -  end;
   1.353 +fun ext_init_data (syn, tsig, ctab, names, data) (kind, e, ext, mrg, prt) =
   1.354 +  (syn, tsig, ctab, names, Data.init data kind e ext mrg prt);
   1.355  
   1.356 -fun make_sign (syn, tsig, ctab, (path, spaces)) data stamps name =
   1.357 -  Sg {tsig = tsig, const_tab = ctab, syn = syn, path = path, spaces = spaces,
   1.358 -    data = data, stamps = ext_stamps stamps name};
   1.359 -
   1.360 -fun extend_sign extfun name decls
   1.361 -    (Sg {tsig, const_tab, syn, path, spaces, data, stamps}) =
   1.362 -  make_sign (extfun (syn, tsig, const_tab, (path, spaces)) decls) data stamps name;
   1.363 +fun ext_put_data (syn, tsig, ctab, names, data) (kind, e) =
   1.364 +  (syn, tsig, ctab, names, Data.put data kind e);
   1.365  
   1.366  
   1.367  (* the external interfaces *)
   1.368 @@ -804,49 +859,48 @@
   1.369  val add_trrules_i    = extend_sign (ext_syn Syntax.extend_trrules_i) "#";
   1.370  val add_path         = extend_sign ext_path "#";
   1.371  val add_space        = extend_sign ext_space "#";
   1.372 +val init_data        = extend_sign ext_init_data "#";
   1.373 +val put_data         = extend_sign ext_put_data "#";
   1.374  fun add_name name sg = extend_sign K name () sg;
   1.375  
   1.376  val make_draft = add_name "#";
   1.377  
   1.378  
   1.379 -(* additional signature data *)
   1.380  
   1.381 -fun map_data f (Sg {tsig, const_tab, syn, path, spaces, data, stamps}) =
   1.382 -  make_sign (syn, tsig, const_tab, (path, spaces)) (f data) stamps "#";
   1.383 +(** merge signatures **)    (*exception TERM*)
   1.384  
   1.385 -fun init_data (kind, e, ext, mrg, prt) =
   1.386 -  map_data (fn d => Data.init d kind e ext mrg prt);
   1.387 +(* merge of sg_refs -- trivial only *)
   1.388  
   1.389 -fun get_data (Sg {data, ...}) = Data.get data;
   1.390 -fun put_data (kind, e) = map_data (fn d => Data.put d kind e);
   1.391 -fun print_data (Sg {data, ...}) kind = Data.print data kind;
   1.392 -
   1.393 -(*prepare extension*)
   1.394 -fun prep_ext sg =
   1.395 -  map_data Data.prep_ext sg |> add_path "/";
   1.396 +fun merge_refs (sgr1 as SgRef (Some (ref sg1)),
   1.397 +        sgr2 as SgRef (Some (ref sg2))) =
   1.398 +      if fast_subsig (sg2, sg1) then sgr1
   1.399 +      else if fast_subsig (sg1, sg2) then sgr2
   1.400 +      else if subsig (sg2, sg1) then sgr1
   1.401 +      else if subsig (sg1, sg2) then sgr2
   1.402 +      else raise TERM ("Attempt to do non-trivial merge of signatures", [])
   1.403 +  | merge_refs _ = sys_error "Sign.merge_refs";
   1.404  
   1.405  
   1.406  
   1.407 -(** merge signatures **)    (*exception TERM*)
   1.408 +(* proper merge *)
   1.409  
   1.410 -fun merge_aux triv_only (sg1, sg2) =
   1.411 -  if fast_subsig (sg2, sg1) then sg1
   1.412 -  else if fast_subsig (sg1, sg2) then sg2
   1.413 -  else if subsig (sg2, sg1) then sg1
   1.414 +fun merge_aux (sg1, sg2) =
   1.415 +  if subsig (sg2, sg1) then sg1
   1.416    else if subsig (sg1, sg2) then sg2
   1.417    else if is_draft sg1 orelse is_draft sg2 then
   1.418 -    raise TERM ("Illegal merge of draft signatures", [])
   1.419 -  else if triv_only then
   1.420 -    raise TERM ("Illegal non-trivial merge of signatures", [])
   1.421 +    raise TERM ("Attempt to merge draft signatures", [])
   1.422    else
   1.423      (*neither is union already; must form union*)
   1.424      let
   1.425 -      val Sg {tsig = tsig1, const_tab = const_tab1, syn = syn1,
   1.426 +      val Sg {id = _, self = _, tsig = tsig1, const_tab = const_tab1, syn = syn1,
   1.427          path = _, spaces = spaces1, data = data1, stamps = stamps1} = sg1;
   1.428 -      val Sg {tsig = tsig2, const_tab = const_tab2, syn = syn2,
   1.429 +      val Sg {id = _, self = _, tsig = tsig2, const_tab = const_tab2, syn = syn2,
   1.430          path = _, spaces = spaces2, data = data2, stamps = stamps2} = sg2;
   1.431  
   1.432  
   1.433 +      val id = ref "";
   1.434 +      val self_ref = ref sg1;			(*dummy value*)
   1.435 +      val self = SgRef (Some self_ref);
   1.436        val stamps = merge_rev_lists stamps1 stamps2;
   1.437        val _ =
   1.438          (case duplicates (stamp_names stamps) of
   1.439 @@ -855,13 +909,12 @@
   1.440              ^ commas_quote dups, []));
   1.441  
   1.442        val tsig = Type.merge_tsigs (tsig1, tsig2);
   1.443 -
   1.444        val const_tab = Symtab.merge (op =) (const_tab1, const_tab2)
   1.445          handle Symtab.DUPS cs =>
   1.446            raise TERM ("Incompatible types for constant(s) " ^ commas_quote cs, []);
   1.447 -
   1.448        val syn = Syntax.merge_syntaxes syn1 syn2;
   1.449  
   1.450 +      val path = [];
   1.451        val kinds = distinct (map fst (spaces1 @ spaces2));
   1.452        val spaces =
   1.453          kinds ~~
   1.454 @@ -869,25 +922,27 @@
   1.455              (map (space_of spaces1) kinds, map (space_of spaces2) kinds);
   1.456  
   1.457        val data = Data.merge (data1, data2);
   1.458 +
   1.459 +      val sign = make_sign (id, self, tsig, const_tab, syn, path, spaces, data, stamps);
   1.460      in
   1.461 -      Sg {tsig = tsig, const_tab = const_tab, syn = syn,
   1.462 -        path = [], spaces = spaces, data = data, stamps = stamps}
   1.463 +      self_ref := sign; sign
   1.464      end;
   1.465  
   1.466 -fun gen_merge triv sgs =
   1.467 -  (case handle_error (merge_aux triv) sgs of
   1.468 +fun merge sg1_sg2 =
   1.469 +  (case handle_error merge_aux sg1_sg2 of
   1.470      OK sg => sg
   1.471    | Error msg => raise TERM (msg, []));
   1.472  
   1.473 -val merge = gen_merge true;
   1.474 -val nontriv_merge = gen_merge false;
   1.475 -
   1.476  
   1.477  
   1.478  (** the Pure signature **)
   1.479  
   1.480 +val dummy_sg = make_sign (ref "", SgRef None, Type.tsig0,
   1.481 +  Symtab.null, Syntax.pure_syn, [], [], Data.empty, []);
   1.482 +
   1.483  val proto_pure =
   1.484 -  make_sign (Syntax.pure_syn, Type.tsig0, Symtab.null, ([], [])) Data.empty [] "#"
   1.485 +  create_sign (SgRef (Some (ref dummy_sg))) [] "#"
   1.486 +    (Syntax.pure_syn, Type.tsig0, Symtab.null, ([], []), Data.empty)
   1.487    |> add_types
   1.488     (("fun", 2, NoSyn) ::
   1.489      ("prop", 0, NoSyn) ::
     2.1 --- a/src/Pure/theory.ML	Tue Oct 21 17:48:06 1997 +0200
     2.2 +++ b/src/Pure/theory.ML	Tue Oct 21 18:09:13 1997 +0200
     2.3 @@ -79,7 +79,7 @@
     2.4      (string -> exn -> unit) -> theory -> theory
     2.5    val get_data		: theory -> string -> exn
     2.6    val put_data		: string * exn -> theory -> theory
     2.7 -  val merge_list	: theory list -> theory
     2.8 +  val prep_ext_merge    : theory list -> theory
     2.9  end;
    2.10  
    2.11  
    2.12 @@ -389,26 +389,26 @@
    2.13  (** merge theories **)
    2.14  
    2.15  (*merge list of theories from left to right, preparing extend*)
    2.16 -fun merge_list thys =
    2.17 +fun prep_ext_merge thys =
    2.18    let
    2.19      fun is_union thy = forall (fn t => subthy (t, thy)) thys;
    2.20      val is_draft = Sign.is_draft o sign_of;
    2.21  
    2.22      fun add_sign (sg, Theory {sign, ...}) =
    2.23 -      Sign.nontriv_merge (sg, sign) handle TERM (msg, _) => error msg;
    2.24 +      Sign.merge (sg, sign) handle TERM (msg, _) => error msg;
    2.25  
    2.26      fun oracles_of (Theory {oracles, ...}) = Symtab.dest oracles;
    2.27      fun eq_ora ((_, (_, s1: stamp)), (_, (_, s2))) = s1 = s2;
    2.28    in
    2.29      if exists is_draft thys then
    2.30 -      raise THEORY ("Illegal merge of draft theories", thys)
    2.31 +      raise THEORY ("Attempt to merge draft theories", thys)
    2.32      else
    2.33        (case find_first is_union thys of
    2.34          Some (Theory {sign, oracles, new_axioms = _, parents = _}) =>
    2.35 -          make_thy (Sign.prep_ext sign) Symtab.null oracles thys
    2.36 +          make_thy (Sign.make_draft sign) Symtab.null oracles thys
    2.37        | None =>
    2.38            make_thy
    2.39 -            (Sign.prep_ext (foldl add_sign (Sign.proto_pure, thys)))
    2.40 +            (Sign.make_draft (foldl add_sign (Sign.proto_pure, thys)))
    2.41              Symtab.null
    2.42              (Symtab.make (gen_distinct eq_ora (flat (map oracles_of thys)))
    2.43                handle Symtab.DUPS names => err_dup_oras names)
    2.44 @@ -417,7 +417,7 @@
    2.45  
    2.46  
    2.47  fun merge_theories name (thy1, thy2) =
    2.48 -  merge_list [thy1, thy2]
    2.49 +  prep_ext_merge [thy1, thy2]
    2.50    |> add_name name;
    2.51  
    2.52  
     3.1 --- a/src/Pure/thm.ML	Tue Oct 21 17:48:06 1997 +0200
     3.2 +++ b/src/Pure/thm.ML	Tue Oct 21 18:09:13 1997 +0200
     3.3 @@ -86,6 +86,7 @@
     3.4    val crep_thm          : thm -> {sign: Sign.sg, der: deriv, maxidx: int,
     3.5                                    shyps: sort list, hyps: cterm list, 
     3.6                                    prop: cterm}
     3.7 +  val sign_of_thm       : thm -> Sign.sg
     3.8    val stamps_of_thm     : thm -> string ref list
     3.9    val transfer		: theory -> thm -> thm
    3.10    val tpairs_of         : thm -> (term * term) list
    3.11 @@ -177,16 +178,17 @@
    3.12  
    3.13  (*certified typs under a signature*)
    3.14  
    3.15 -datatype ctyp = Ctyp of {sign: Sign.sg, T: typ};
    3.16 +datatype ctyp = Ctyp of {sign_ref: Sign.sg_ref, T: typ};
    3.17  
    3.18 -fun rep_ctyp (Ctyp args) = args;
    3.19 +(* FIXME tune!? *)
    3.20 +fun rep_ctyp (Ctyp {sign_ref, T}) = {sign = Sign.deref sign_ref, T = T};
    3.21  fun typ_of (Ctyp {T, ...}) = T;
    3.22  
    3.23  fun ctyp_of sign T =
    3.24 -  Ctyp {sign = sign, T = Sign.certify_typ sign T};
    3.25 +  Ctyp {sign_ref = Sign.self_ref sign, T = Sign.certify_typ sign T};
    3.26  
    3.27  fun read_ctyp sign s =
    3.28 -  Ctyp {sign = sign, T = Sign.read_typ (sign, K None) s};
    3.29 +  Ctyp {sign_ref = Sign.self_ref sign, T = Sign.read_typ (sign, K None) s};
    3.30  
    3.31  
    3.32  
    3.33 @@ -194,60 +196,63 @@
    3.34  
    3.35  (*certified terms under a signature, with checked typ and maxidx of Vars*)
    3.36  
    3.37 -datatype cterm = Cterm of {sign: Sign.sg, t: term, T: typ, maxidx: int};
    3.38 +datatype cterm = Cterm of {sign_ref: Sign.sg_ref, t: term, T: typ, maxidx: int};
    3.39  
    3.40 -fun rep_cterm (Cterm args) = args;
    3.41 +(* FIXME tune!? *)
    3.42 +fun rep_cterm (Cterm {sign_ref, t, T, maxidx}) =
    3.43 +  {sign = Sign.deref sign_ref, t = t, T = T, maxidx = maxidx};
    3.44 +
    3.45  fun term_of (Cterm {t, ...}) = t;
    3.46  
    3.47 -fun ctyp_of_term (Cterm {sign, T, ...}) = Ctyp {sign=sign, T=T};
    3.48 +fun ctyp_of_term (Cterm {sign_ref, T, ...}) = Ctyp {sign_ref = sign_ref, T = T};
    3.49  
    3.50  (*create a cterm by checking a "raw" term with respect to a signature*)
    3.51  fun cterm_of sign tm =
    3.52    let val (t, T, maxidx) = Sign.certify_term sign tm
    3.53 -  in  Cterm {sign = sign, t = t, T = T, maxidx = maxidx}
    3.54 +  in  Cterm {sign_ref = Sign.self_ref sign, t = t, T = T, maxidx = maxidx}
    3.55    end;
    3.56  
    3.57 -fun cterm_fun f (Cterm {sign, t, ...}) = cterm_of sign (f t);
    3.58 +fun cterm_fun f (Cterm {sign_ref, t, ...}) = cterm_of (Sign.deref sign_ref) (f t);
    3.59  
    3.60  
    3.61  exception CTERM of string;
    3.62  
    3.63  (*Destruct application in cterms*)
    3.64 -fun dest_comb (Cterm{sign, T, maxidx, t = A $ B}) =
    3.65 +fun dest_comb (Cterm {sign_ref, T, maxidx, t = A $ B}) =
    3.66        let val typeA = fastype_of A;
    3.67            val typeB =
    3.68              case typeA of Type("fun",[S,T]) => S
    3.69                          | _ => error "Function type expected in dest_comb";
    3.70        in
    3.71 -      (Cterm {sign=sign, maxidx=maxidx, t=A, T=typeA},
    3.72 -       Cterm {sign=sign, maxidx=maxidx, t=B, T=typeB})
    3.73 +      (Cterm {sign_ref=sign_ref, maxidx=maxidx, t=A, T=typeA},
    3.74 +       Cterm {sign_ref=sign_ref, maxidx=maxidx, t=B, T=typeB})
    3.75        end
    3.76    | dest_comb _ = raise CTERM "dest_comb";
    3.77  
    3.78  (*Destruct abstraction in cterms*)
    3.79 -fun dest_abs (Cterm {sign, T as Type("fun",[_,S]), maxidx, t=Abs(x,ty,M)}) = 
    3.80 +fun dest_abs (Cterm {sign_ref, T as Type("fun",[_,S]), maxidx, t=Abs(x,ty,M)}) = 
    3.81        let val (y,N) = variant_abs (x,ty,M)
    3.82 -      in (Cterm {sign = sign, T = ty, maxidx = 0, t = Free(y,ty)},
    3.83 -          Cterm {sign = sign, T = S, maxidx = maxidx, t = N})
    3.84 +      in (Cterm {sign_ref = sign_ref, T = ty, maxidx = 0, t = Free(y,ty)},
    3.85 +          Cterm {sign_ref = sign_ref, T = S, maxidx = maxidx, t = N})
    3.86        end
    3.87    | dest_abs _ = raise CTERM "dest_abs";
    3.88  
    3.89  (*Makes maxidx precise: it is often too big*)
    3.90 -fun adjust_maxidx (ct as Cterm {sign, T, t, maxidx, ...}) =
    3.91 +fun adjust_maxidx (ct as Cterm {sign_ref, T, t, maxidx, ...}) =
    3.92    if maxidx = ~1 then ct 
    3.93 -  else  Cterm {sign = sign, T = T, maxidx = maxidx_of_term t, t = t};
    3.94 +  else  Cterm {sign_ref = sign_ref, T = T, maxidx = maxidx_of_term t, t = t};
    3.95  
    3.96  (*Form cterm out of a function and an argument*)
    3.97 -fun capply (Cterm {t=f, sign=sign1, T=Type("fun",[dty,rty]), maxidx=maxidx1})
    3.98 -           (Cterm {t=x, sign=sign2, T, maxidx=maxidx2}) =
    3.99 -      if T = dty then Cterm{t=f$x, sign=Sign.merge(sign1,sign2), T=rty,
   3.100 +fun capply (Cterm {t=f, sign_ref=sign_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1})
   3.101 +           (Cterm {t=x, sign_ref=sign_ref2, T, maxidx=maxidx2}) =
   3.102 +      if T = dty then Cterm{t=f$x, sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), T=rty,
   3.103                              maxidx=Int.max(maxidx1, maxidx2)}
   3.104        else raise CTERM "capply: types don't agree"
   3.105    | capply _ _ = raise CTERM "capply: first arg is not a function"
   3.106  
   3.107 -fun cabs (Cterm {t=Free(a,ty), sign=sign1, T=T1, maxidx=maxidx1})
   3.108 -         (Cterm {t=t2, sign=sign2, T=T2, maxidx=maxidx2}) =
   3.109 -      Cterm {t=absfree(a,ty,t2), sign=Sign.merge(sign1,sign2),
   3.110 +fun cabs (Cterm {t=Free(a,ty), sign_ref=sign_ref1, T=T1, maxidx=maxidx1})
   3.111 +         (Cterm {t=t2, sign_ref=sign_ref2, T=T2, maxidx=maxidx2}) =
   3.112 +      Cterm {t=absfree(a,ty,t2), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2),
   3.113               T = ty --> T2, maxidx=Int.max(maxidx1, maxidx2)}
   3.114    | cabs _ _ = raise CTERM "cabs: first arg is not a free variable";
   3.115  
   3.116 @@ -262,7 +267,7 @@
   3.117        handle TYPE (msg, _, _) => error msg;
   3.118      val ts = Syntax.read (#syn (Sign.rep_sg sign)) T' a;
   3.119      val (_, t', tye) =
   3.120 -          Sign.infer_types sign types sorts used freeze (ts, T');
   3.121 +      Sign.infer_types sign types sorts used freeze (ts, T');
   3.122      val ct = cterm_of sign t'
   3.123        handle TYPE (msg, _, _) => error msg
   3.124             | TERM (msg, _) => error msg;
   3.125 @@ -384,19 +389,22 @@
   3.126  (*** Meta theorems ***)
   3.127  
   3.128  datatype thm = Thm of
   3.129 -  {sign: Sign.sg,               (*signature for hyps and prop*)
   3.130 -   der: deriv,                  (*derivation*)
   3.131 -   maxidx: int,                 (*maximum index of any Var or TVar*)
   3.132 -   shyps: sort list,            (*sort hypotheses*)
   3.133 -   hyps: term list,             (*hypotheses*)
   3.134 -   prop: term};                 (*conclusion*)
   3.135 + {sign_ref: Sign.sg_ref,       (*mutable reference to signature*)
   3.136 +  der: deriv,                  (*derivation*)
   3.137 +  maxidx: int,                 (*maximum index of any Var or TVar*)
   3.138 +  shyps: sort list,            (*sort hypotheses*)
   3.139 +  hyps: term list,             (*hypotheses*)
   3.140 +  prop: term};                 (*conclusion*)
   3.141  
   3.142 -fun rep_thm (Thm args) = args;
   3.143 +(* FIXME tune!? *)
   3.144 +fun rep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
   3.145 +  {sign = Sign.deref sign_ref, der = der, maxidx = maxidx,
   3.146 +    shyps = shyps, hyps = hyps, prop = prop};
   3.147  
   3.148  (*Version of rep_thm returning cterms instead of terms*)
   3.149 -fun crep_thm (Thm {sign, der, maxidx, shyps, hyps, prop}) =
   3.150 -  let fun ctermf max t = Cterm{sign=sign, t=t, T=propT, maxidx=max};
   3.151 -  in {sign=sign, der=der, maxidx=maxidx, shyps=shyps,
   3.152 +fun crep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
   3.153 +  let fun ctermf max t = Cterm{sign_ref=sign_ref, t=t, T=propT, maxidx=max};
   3.154 +  in {sign = Sign.deref sign_ref, der = der, maxidx = maxidx, shyps = shyps,
   3.155        hyps = map (ctermf ~1) hyps,
   3.156        prop = ctermf maxidx prop}
   3.157    end;
   3.158 @@ -405,21 +413,23 @@
   3.159  exception THM of string * int * thm list;
   3.160  
   3.161  
   3.162 -val stamps_of_thm = #stamps o Sign.rep_sg o #sign o rep_thm;
   3.163 +fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref;
   3.164 +val stamps_of_thm = #stamps o Sign.rep_sg o sign_of_thm;
   3.165  
   3.166  (*merge signatures of two theorems; raise exception if incompatible*)
   3.167 -fun merge_thm_sgs (th1, th2) =
   3.168 -  Sign.merge (pairself (#sign o rep_thm) (th1, th2))
   3.169 -    handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]);
   3.170 +fun merge_thm_sgs
   3.171 +    (th1 as Thm {sign_ref = sgr1, ...}, th2 as Thm {sign_ref = sgr2, ...}) =
   3.172 +  Sign.merge_refs (sgr1, sgr2) handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]);
   3.173  
   3.174 -(*transfer thm to super theory*)
   3.175 +(*transfer thm to super theory (non-destructive)*)
   3.176  fun transfer thy thm =
   3.177    let
   3.178 -    val Thm {sign, der, maxidx, shyps, hyps, prop} = thm;
   3.179 +    val Thm {sign_ref, der, maxidx, shyps, hyps, prop} = thm;
   3.180 +    val sign = Sign.deref sign_ref;
   3.181      val sign' = #sign (rep_theory thy);
   3.182    in
   3.183      if Sign.subsig (sign, sign') then
   3.184 -      Thm {sign = sign', der = der, maxidx = maxidx,
   3.185 +      Thm {sign_ref = Sign.self_ref sign', der = der, maxidx = maxidx,
   3.186          shyps = shyps, hyps = hyps, prop = prop}
   3.187      else raise THM ("transfer: not a super theory", 0, [thm])
   3.188    end;
   3.189 @@ -439,8 +449,8 @@
   3.190  fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop;
   3.191  
   3.192  (*the statement of any thm is a cterm*)
   3.193 -fun cprop_of (Thm {sign, maxidx, prop, ...}) =
   3.194 -  Cterm {sign = sign, maxidx = maxidx, T = propT, t = prop};
   3.195 +fun cprop_of (Thm {sign_ref, maxidx, prop, ...}) =
   3.196 +  Cterm {sign_ref = sign_ref, maxidx = maxidx, T = propT, t = prop};
   3.197  
   3.198  
   3.199  
   3.200 @@ -491,11 +501,11 @@
   3.201  (*preserve sort contexts of rule premises and substituted types*)
   3.202  fun fix_shyps thms Ts thm =
   3.203    let
   3.204 -    val Thm {sign, der, maxidx, hyps, prop, ...} = thm;
   3.205 +    val Thm {sign_ref, der, maxidx, hyps, prop, ...} = thm;
   3.206      val shyps =
   3.207        add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, [])));
   3.208    in
   3.209 -    Thm {sign = sign, 
   3.210 +    Thm {sign_ref = sign_ref,
   3.211           der = der,             (*No new derivation, as other rules call this*)
   3.212           maxidx = maxidx,
   3.213           shyps = shyps, hyps = hyps, prop = prop}
   3.214 @@ -509,12 +519,12 @@
   3.215  (*remove extra sorts that are known to be syntactically non-empty*)
   3.216  fun strip_shyps thm =
   3.217    let
   3.218 -    val Thm {sign, der, maxidx, shyps, hyps, prop} = thm;
   3.219 +    val Thm {sign_ref, der, maxidx, shyps, hyps, prop} = thm;
   3.220      val sorts = add_thm_sorts (thm, []);
   3.221 -    val maybe_empty = not o Sign.nonempty_sort sign sorts;
   3.222 +    val maybe_empty = not o Sign.nonempty_sort (Sign.deref sign_ref) sorts;
   3.223      val shyps' = filter (fn S => mem_sort(S,sorts) orelse maybe_empty S) shyps;
   3.224    in
   3.225 -    Thm {sign = sign, der = der, maxidx = maxidx,
   3.226 +    Thm {sign_ref = sign_ref, der = der, maxidx = maxidx,
   3.227           shyps =
   3.228           (if eq_set_sort (shyps',sorts) orelse 
   3.229               not (!force_strip_shyps) then shyps'
   3.230 @@ -536,7 +546,7 @@
   3.231      [] => thm
   3.232    | xshyps =>
   3.233        let
   3.234 -        val Thm {sign, der, maxidx, shyps, hyps, prop} = thm;
   3.235 +        val Thm {sign_ref, der, maxidx, shyps, hyps, prop} = thm;
   3.236          val shyps' = ins_sort (logicS, shyps \\ xshyps);
   3.237          val used_names = foldr add_term_tfree_names (prop :: hyps, []);
   3.238          val names =
   3.239 @@ -546,7 +556,7 @@
   3.240          fun mk_insort (T, S) = map (Logic.mk_inclass o pair T) S;
   3.241          val sort_hyps = List.concat (map2 mk_insort (tfrees, xshyps));
   3.242        in
   3.243 -        Thm {sign = sign, 
   3.244 +        Thm {sign_ref = sign_ref, 
   3.245               der = infer_derivs (Implies_intr_shyps, [der]), 
   3.246               maxidx = maxidx, 
   3.247               shyps = shyps',
   3.248 @@ -566,7 +576,7 @@
   3.249            let val {sign, new_axioms, parents, ...} = rep_theory thy
   3.250            in case Symtab.lookup (new_axioms, name) of
   3.251                  Some t => fix_shyps [] []
   3.252 -                           (Thm {sign = sign, 
   3.253 +                           (Thm {sign_ref = Sign.self_ref sign,
   3.254                                   der = infer_derivs (Axiom(theory,name), []),
   3.255                                   maxidx = maxidx_of_term t,
   3.256                                   shyps = [], 
   3.257 @@ -586,8 +596,8 @@
   3.258      (Symtab.dest (#new_axioms (rep_theory thy)));
   3.259  
   3.260  (*Attach a label to a theorem to make proof objects more readable*)
   3.261 -fun name_thm (name, th as Thm {sign, der, maxidx, shyps, hyps, prop}) = 
   3.262 -    Thm {sign = sign, 
   3.263 +fun name_thm (name, th as Thm {sign_ref, der, maxidx, shyps, hyps, prop}) = 
   3.264 +    Thm {sign_ref = sign_ref, 
   3.265           der = Join (Theorem name, [der]),
   3.266           maxidx = maxidx,
   3.267           shyps = shyps, 
   3.268 @@ -597,8 +607,8 @@
   3.269  
   3.270  (*Compression of theorems -- a separate rule, not integrated with the others,
   3.271    as it could be slow.*)
   3.272 -fun compress (Thm {sign, der, maxidx, shyps, hyps, prop}) = 
   3.273 -    Thm {sign = sign, 
   3.274 +fun compress (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) = 
   3.275 +    Thm {sign_ref = sign_ref, 
   3.276           der = der,     (*No derivation recorded!*)
   3.277           maxidx = maxidx,
   3.278           shyps = shyps, 
   3.279 @@ -612,9 +622,9 @@
   3.280  (*Check that term does not contain same var with different typing/sorting.
   3.281    If this check must be made, recalculate maxidx in hope of preventing its
   3.282    recurrence.*)
   3.283 -fun nodup_Vars (thm as Thm{sign, der, maxidx, shyps, hyps, prop}) s =
   3.284 +fun nodup_Vars (thm as Thm{sign_ref, der, maxidx, shyps, hyps, prop}) s =
   3.285    (Sign.nodup_Vars prop; 
   3.286 -   Thm {sign = sign, 
   3.287 +   Thm {sign_ref = sign_ref, 
   3.288           der = der,     
   3.289           maxidx = maxidx_of_term prop,
   3.290           shyps = shyps, 
   3.291 @@ -629,13 +639,13 @@
   3.292  
   3.293  (*The assumption rule A|-A in a theory*)
   3.294  fun assume ct : thm =
   3.295 -  let val {sign, t=prop, T, maxidx} = rep_cterm ct
   3.296 +  let val Cterm {sign_ref, t=prop, T, maxidx} = ct
   3.297    in  if T<>propT then
   3.298          raise THM("assume: assumptions must have type prop", 0, [])
   3.299        else if maxidx <> ~1 then
   3.300          raise THM("assume: assumptions may not contain scheme variables",
   3.301                    maxidx, [])
   3.302 -      else Thm{sign   = sign, 
   3.303 +      else Thm{sign_ref   = sign_ref,
   3.304                 der    = infer_derivs (Assume ct, []), 
   3.305                 maxidx = ~1, 
   3.306                 shyps  = add_term_sorts(prop,[]), 
   3.307 @@ -650,12 +660,12 @@
   3.308    -------
   3.309    A ==> B
   3.310  *)
   3.311 -fun implies_intr cA (thB as Thm{sign,der,maxidx,hyps,prop,...}) : thm =
   3.312 -  let val {sign=signA, t=A, T, maxidx=maxidxA} = rep_cterm cA
   3.313 +fun implies_intr cA (thB as Thm{sign_ref,der,maxidx,hyps,prop,...}) : thm =
   3.314 +  let val Cterm {sign_ref=sign_refA, t=A, T, maxidx=maxidxA} = cA
   3.315    in  if T<>propT then
   3.316          raise THM("implies_intr: assumptions must have type prop", 0, [thB])
   3.317        else fix_shyps [thB] []
   3.318 -        (Thm{sign = Sign.merge (sign,signA),  
   3.319 +        (Thm{sign_ref = Sign.merge_refs (sign_ref,sign_refA),  
   3.320               der = infer_derivs (Implies_intr cA, [der]),
   3.321               maxidx = Int.max(maxidxA, maxidx),
   3.322               shyps = [],
   3.323 @@ -673,13 +683,13 @@
   3.324  *)
   3.325  fun implies_elim thAB thA : thm =
   3.326      let val Thm{maxidx=maxA, der=derA, hyps=hypsA, prop=propA,...} = thA
   3.327 -        and Thm{sign, der, maxidx, hyps, prop,...} = thAB;
   3.328 +        and Thm{sign_ref, der, maxidx, hyps, prop,...} = thAB;
   3.329          fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA])
   3.330      in  case prop of
   3.331              imp$A$B =>
   3.332                  if imp=implies andalso  A aconv propA
   3.333                  then fix_shyps [thAB, thA] []
   3.334 -                       (Thm{sign= merge_thm_sgs(thAB,thA),
   3.335 +                       (Thm{sign_ref= merge_thm_sgs(thAB,thA),
   3.336                              der = infer_derivs (Implies_elim, [der,derA]),
   3.337                              maxidx = Int.max(maxA,maxidx),
   3.338                              shyps = [],
   3.339 @@ -694,10 +704,10 @@
   3.340    -----
   3.341    !!x.A
   3.342  *)
   3.343 -fun forall_intr cx (th as Thm{sign,der,maxidx,hyps,prop,...}) =
   3.344 +fun forall_intr cx (th as Thm{sign_ref,der,maxidx,hyps,prop,...}) =
   3.345    let val x = term_of cx;
   3.346        fun result(a,T) = fix_shyps [th] []
   3.347 -        (Thm{sign = sign, 
   3.348 +        (Thm{sign_ref = sign_ref, 
   3.349               der = infer_derivs (Forall_intr cx, [der]),
   3.350               maxidx = maxidx,
   3.351               shyps = [],
   3.352 @@ -717,14 +727,14 @@
   3.353    ------
   3.354    A[t/x]
   3.355  *)
   3.356 -fun forall_elim ct (th as Thm{sign,der,maxidx,hyps,prop,...}) : thm =
   3.357 -  let val {sign=signt, t, T, maxidx=maxt} = rep_cterm ct
   3.358 +fun forall_elim ct (th as Thm{sign_ref,der,maxidx,hyps,prop,...}) : thm =
   3.359 +  let val Cterm {sign_ref=sign_reft, t, T, maxidx=maxt} = ct
   3.360    in  case prop of
   3.361          Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A =>
   3.362            if T<>qary then
   3.363                raise THM("forall_elim: type mismatch", 0, [th])
   3.364            else let val thm = fix_shyps [th] []
   3.365 -                    (Thm{sign= Sign.merge(sign,signt),
   3.366 +                    (Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft),
   3.367                           der = infer_derivs (Forall_elim ct, [der]),
   3.368                           maxidx = Int.max(maxidx, maxt),
   3.369                           shyps = [],
   3.370 @@ -744,7 +754,7 @@
   3.371  
   3.372  (* Definition of the relation =?= *)
   3.373  val flexpair_def = fix_shyps [] []
   3.374 -  (Thm{sign= Sign.proto_pure, 
   3.375 +  (Thm{sign_ref= Sign.self_ref Sign.proto_pure, 
   3.376         der = Join(Axiom(pure_thy, "flexpair_def"), []),
   3.377         shyps = [], 
   3.378         hyps = [], 
   3.379 @@ -754,9 +764,9 @@
   3.380  
   3.381  (*The reflexivity rule: maps  t   to the theorem   t==t   *)
   3.382  fun reflexive ct =
   3.383 -  let val {sign, t, T, maxidx} = rep_cterm ct
   3.384 +  let val Cterm {sign_ref, t, T, maxidx} = ct
   3.385    in  fix_shyps [] []
   3.386 -       (Thm{sign= sign, 
   3.387 +       (Thm{sign_ref= sign_ref, 
   3.388              der = infer_derivs (Reflexive ct, []),
   3.389              shyps = [],
   3.390              hyps = [], 
   3.391 @@ -769,11 +779,11 @@
   3.392    ----
   3.393    u==t
   3.394  *)
   3.395 -fun symmetric (th as Thm{sign,der,maxidx,shyps,hyps,prop}) =
   3.396 +fun symmetric (th as Thm{sign_ref,der,maxidx,shyps,hyps,prop}) =
   3.397    case prop of
   3.398        (eq as Const("==",_)) $ t $ u =>
   3.399          (*no fix_shyps*)
   3.400 -          Thm{sign = sign,
   3.401 +          Thm{sign_ref = sign_ref,
   3.402                der = infer_derivs (Symmetric, [der]),
   3.403                maxidx = maxidx,
   3.404                shyps = shyps,
   3.405 @@ -795,7 +805,7 @@
   3.406            if not (u aconv u') then err"middle term"
   3.407            else let val thm =      
   3.408                fix_shyps [th1, th2] []
   3.409 -                (Thm{sign= merge_thm_sgs(th1,th2), 
   3.410 +                (Thm{sign_ref= merge_thm_sgs(th1,th2), 
   3.411                       der = infer_derivs (Transitive, [der1, der2]),
   3.412                       maxidx = Int.max(max1,max2), 
   3.413                       shyps = [],
   3.414 @@ -810,10 +820,10 @@
   3.415  
   3.416  (*Beta-conversion: maps (%x.t)(u) to the theorem (%x.t)(u) == t[u/x] *)
   3.417  fun beta_conversion ct =
   3.418 -  let val {sign, t, T, maxidx} = rep_cterm ct
   3.419 +  let val Cterm {sign_ref, t, T, maxidx} = ct
   3.420    in  case t of
   3.421            Abs(_,_,bodt) $ u => fix_shyps [] []
   3.422 -            (Thm{sign = sign,  
   3.423 +            (Thm{sign_ref = sign_ref,  
   3.424                   der = infer_derivs (Beta_conversion ct, []),
   3.425                   maxidx = maxidx,
   3.426                   shyps = [],
   3.427 @@ -827,7 +837,7 @@
   3.428    ------------
   3.429       f == g
   3.430  *)
   3.431 -fun extensional (th as Thm{sign, der, maxidx,shyps,hyps,prop}) =
   3.432 +fun extensional (th as Thm{sign_ref, der, maxidx,shyps,hyps,prop}) =
   3.433    case prop of
   3.434      (Const("==",_)) $ (f$x) $ (g$y) =>
   3.435        let fun err(msg) = raise THM("extensional: "^msg, 0, [th])
   3.436 @@ -841,7 +851,7 @@
   3.437                    then err"variable free in functions"   else  ()
   3.438                | _ => err"not a variable");
   3.439            (*no fix_shyps*)
   3.440 -          Thm{sign = sign,
   3.441 +          Thm{sign_ref = sign_ref,
   3.442                der = infer_derivs (Extensional, [der]),
   3.443                maxidx = maxidx,
   3.444                shyps = shyps,
   3.445 @@ -856,13 +866,13 @@
   3.446    ------------
   3.447    %x.t == %x.u
   3.448  *)
   3.449 -fun abstract_rule a cx (th as Thm{sign,der,maxidx,hyps,prop,...}) =
   3.450 +fun abstract_rule a cx (th as Thm{sign_ref,der,maxidx,hyps,prop,...}) =
   3.451    let val x = term_of cx;
   3.452        val (t,u) = Logic.dest_equals prop
   3.453              handle TERM _ =>
   3.454                  raise THM("abstract_rule: premise not an equality", 0, [th])
   3.455        fun result T = fix_shyps [th] []
   3.456 -          (Thm{sign = sign,
   3.457 +          (Thm{sign_ref = sign_ref,
   3.458                 der = infer_derivs (Abstract_rule (a,cx), [der]),
   3.459                 maxidx = maxidx, 
   3.460                 shyps = [], 
   3.461 @@ -900,7 +910,7 @@
   3.462         (Const("==",_) $ f $ g, Const("==",_) $ t $ u) =>
   3.463            let val _   = chktypes (f,t)
   3.464                val thm = (*no fix_shyps*)
   3.465 -                        Thm{sign = merge_thm_sgs(th1,th2), 
   3.466 +                        Thm{sign_ref = merge_thm_sgs(th1,th2), 
   3.467                              der = infer_derivs (Combination, [der1, der2]),
   3.468                              maxidx = Int.max(max1,max2), 
   3.469                              shyps = union_sort(shyps1,shyps2),
   3.470 @@ -930,7 +940,7 @@
   3.471            if A aconv A' andalso B aconv B'
   3.472            then
   3.473              (*no fix_shyps*)
   3.474 -              Thm{sign = merge_thm_sgs(th1,th2),
   3.475 +              Thm{sign_ref = merge_thm_sgs(th1,th2),
   3.476                    der = infer_derivs (Equal_intr, [der1, der2]),
   3.477                    maxidx = Int.max(max1,max2),
   3.478                    shyps = union_sort(shyps1,shyps2),
   3.479 @@ -954,7 +964,7 @@
   3.480         Const("==",_) $ A $ B =>
   3.481            if not (prop2 aconv A) then err"not equal"  else
   3.482              fix_shyps [th1, th2] []
   3.483 -              (Thm{sign= merge_thm_sgs(th1,th2), 
   3.484 +              (Thm{sign_ref= merge_thm_sgs(th1,th2), 
   3.485                     der = infer_derivs (Equal_elim, [der1, der2]),
   3.486                     maxidx = Int.max(max1,max2),
   3.487                     shyps = [],
   3.488 @@ -969,9 +979,9 @@
   3.489  
   3.490  (*Discharge all hypotheses.  Need not verify cterms or call fix_shyps.
   3.491    Repeated hypotheses are discharged only once;  fold cannot do this*)
   3.492 -fun implies_intr_hyps (Thm{sign, der, maxidx, shyps, hyps=A::As, prop}) =
   3.493 +fun implies_intr_hyps (Thm{sign_ref, der, maxidx, shyps, hyps=A::As, prop}) =
   3.494        implies_intr_hyps (*no fix_shyps*)
   3.495 -            (Thm{sign = sign, 
   3.496 +            (Thm{sign_ref = sign_ref, 
   3.497                   der = infer_derivs (Implies_intr_hyps, [der]), 
   3.498                   maxidx = maxidx, 
   3.499                   shyps = shyps,
   3.500 @@ -983,7 +993,7 @@
   3.501    Instantiates the theorem and deletes trivial tpairs.
   3.502    Resulting sequence may contain multiple elements if the tpairs are
   3.503      not all flex-flex. *)
   3.504 -fun flexflex_rule (th as Thm{sign, der, maxidx, hyps, prop,...}) =
   3.505 +fun flexflex_rule (th as Thm{sign_ref, der, maxidx, hyps, prop,...}) =
   3.506    let fun newthm env =
   3.507            if Envir.is_empty env then th
   3.508            else
   3.509 @@ -993,7 +1003,7 @@
   3.510                val distpairs = filter (not o op aconv) tpairs
   3.511                val newprop = Logic.list_flexpairs(distpairs, horn)
   3.512            in  fix_shyps [th] (env_codT env)
   3.513 -                (Thm{sign = sign, 
   3.514 +                (Thm{sign_ref = sign_ref, 
   3.515                       der = infer_derivs (Flexflex_rule env, [der]), 
   3.516                       maxidx = maxidx_of_term newprop, 
   3.517                       shyps = [], 
   3.518 @@ -1002,7 +1012,7 @@
   3.519            end;
   3.520        val (tpairs,_) = Logic.strip_flexpairs prop
   3.521    in Sequence.maps newthm
   3.522 -            (Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs))
   3.523 +            (Unify.smash_unifiers(Sign.deref sign_ref, Envir.empty maxidx, tpairs))
   3.524    end;
   3.525  
   3.526  (*Instantiation of Vars
   3.527 @@ -1015,31 +1025,33 @@
   3.528  fun instl_ok ts = forall is_Var ts andalso null(findrep ts);
   3.529  
   3.530  (*For instantiate: process pair of cterms, merge theories*)
   3.531 -fun add_ctpair ((ct,cu), (sign,tpairs)) =
   3.532 -  let val {sign=signt, t=t, T= T, ...} = rep_cterm ct
   3.533 -      and {sign=signu, t=u, T= U, ...} = rep_cterm cu
   3.534 -  in  if T=U  then (Sign.merge(sign, Sign.merge(signt, signu)), (t,u)::tpairs)
   3.535 -      else raise TYPE("add_ctpair", [T,U], [t,u])
   3.536 +fun add_ctpair ((ct,cu), (sign_ref,tpairs)) =
   3.537 +  let val Cterm {sign_ref=sign_reft, t=t, T= T, ...} = ct
   3.538 +      and Cterm {sign_ref=sign_refu, t=u, T= U, ...} = cu
   3.539 +  in
   3.540 +    if T=U then
   3.541 +      (Sign.merge_refs (sign_ref, Sign.merge_refs (sign_reft, sign_refu)), (t,u)::tpairs)
   3.542 +    else raise TYPE("add_ctpair", [T,U], [t,u])
   3.543    end;
   3.544  
   3.545 -fun add_ctyp ((v,ctyp), (sign',vTs)) =
   3.546 -  let val {T,sign} = rep_ctyp ctyp
   3.547 -  in (Sign.merge(sign,sign'), (v,T)::vTs) end;
   3.548 +fun add_ctyp ((v,ctyp), (sign_ref',vTs)) =
   3.549 +  let val Ctyp {T,sign_ref} = ctyp
   3.550 +  in (Sign.merge_refs(sign_ref,sign_ref'), (v,T)::vTs) end;
   3.551  
   3.552  (*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
   3.553    Instantiates distinct Vars by terms of same type.
   3.554    Normalizes the new theorem! *)
   3.555  fun instantiate ([], []) th = th
   3.556 -  | instantiate (vcTs,ctpairs)  (th as Thm{sign,der,maxidx,hyps,prop,...}) =
   3.557 -  let val (newsign,tpairs) = foldr add_ctpair (ctpairs, (sign,[]));
   3.558 -      val (newsign,vTs) = foldr add_ctyp (vcTs, (newsign,[]));
   3.559 +  | instantiate (vcTs,ctpairs)  (th as Thm{sign_ref,der,maxidx,hyps,prop,...}) =
   3.560 +  let val (newsign_ref,tpairs) = foldr add_ctpair (ctpairs, (sign_ref,[]));
   3.561 +      val (newsign_ref,vTs) = foldr add_ctyp (vcTs, (newsign_ref,[]));
   3.562        val newprop =
   3.563              Envir.norm_term (Envir.empty 0)
   3.564                (subst_atomic tpairs
   3.565 -               (Type.inst_term_tvars(#tsig(Sign.rep_sg newsign),vTs) prop))
   3.566 +               (Type.inst_term_tvars(Sign.tsig_of (Sign.deref newsign_ref),vTs) prop))
   3.567        val newth =
   3.568              fix_shyps [th] (map snd vTs)
   3.569 -              (Thm{sign = newsign, 
   3.570 +              (Thm{sign_ref = newsign_ref, 
   3.571                     der = infer_derivs (Instantiate(vcTs,ctpairs), [der]), 
   3.572                     maxidx = maxidx_of_term newprop, 
   3.573                     shyps = [],
   3.574 @@ -1059,11 +1071,11 @@
   3.575  (*The trivial implication A==>A, justified by assume and forall rules.
   3.576    A can contain Vars, not so for assume!   *)
   3.577  fun trivial ct : thm =
   3.578 -  let val {sign, t=A, T, maxidx} = rep_cterm ct
   3.579 +  let val Cterm {sign_ref, t=A, T, maxidx} = ct
   3.580    in  if T<>propT then
   3.581              raise THM("trivial: the term must have type prop", 0, [])
   3.582        else fix_shyps [] []
   3.583 -        (Thm{sign = sign, 
   3.584 +        (Thm{sign_ref = sign_ref, 
   3.585               der = infer_derivs (Trivial ct, []), 
   3.586               maxidx = maxidx, 
   3.587               shyps = [], 
   3.588 @@ -1074,12 +1086,12 @@
   3.589  (*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *)
   3.590  fun class_triv thy c =
   3.591    let val sign = sign_of thy;
   3.592 -      val Cterm {t, maxidx, ...} =
   3.593 +      val Cterm {sign_ref, t, maxidx, ...} =
   3.594            cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c))
   3.595              handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
   3.596    in
   3.597      fix_shyps [] []
   3.598 -      (Thm {sign = sign, 
   3.599 +      (Thm {sign_ref = sign_ref, 
   3.600              der = infer_derivs (Class_triv(thy,c), []), 
   3.601              maxidx = maxidx, 
   3.602              shyps = [], 
   3.603 @@ -1089,10 +1101,10 @@
   3.604  
   3.605  
   3.606  (* Replace all TFrees not in the hyps by new TVars *)
   3.607 -fun varifyT(Thm{sign,der,maxidx,shyps,hyps,prop}) =
   3.608 +fun varifyT(Thm{sign_ref,der,maxidx,shyps,hyps,prop}) =
   3.609    let val tfrees = foldr add_term_tfree_names (hyps,[])
   3.610    in let val thm = (*no fix_shyps*)
   3.611 -    Thm{sign = sign, 
   3.612 +    Thm{sign_ref = sign_ref, 
   3.613          der = infer_derivs (VarifyT, [der]), 
   3.614          maxidx = Int.max(0,maxidx), 
   3.615          shyps = shyps, 
   3.616 @@ -1104,10 +1116,10 @@
   3.617    end;
   3.618  
   3.619  (* Replace all TVars by new TFrees *)
   3.620 -fun freezeT(Thm{sign,der,maxidx,shyps,hyps,prop}) =
   3.621 +fun freezeT(Thm{sign_ref,der,maxidx,shyps,hyps,prop}) =
   3.622    let val (prop',_) = Type.freeze_thaw prop
   3.623    in (*no fix_shyps*)
   3.624 -    Thm{sign = sign, 
   3.625 +    Thm{sign_ref = sign_ref, 
   3.626          der = infer_derivs (FreezeT, [der]),
   3.627          maxidx = maxidx_of_term prop',
   3.628          shyps = shyps,
   3.629 @@ -1130,15 +1142,15 @@
   3.630  (*Increment variables and parameters of orule as required for
   3.631    resolution with goal i of state. *)
   3.632  fun lift_rule (state, i) orule =
   3.633 -  let val Thm{shyps=sshyps, prop=sprop, maxidx=smax, sign=ssign,...} = state
   3.634 +  let val Thm{shyps=sshyps, prop=sprop, maxidx=smax, sign_ref=ssign_ref,...} = state
   3.635        val (Bi::_, _) = Logic.strip_prems(i, [], Logic.skip_flexpairs sprop)
   3.636          handle TERM _ => raise THM("lift_rule", i, [orule,state])
   3.637 -      val ct_Bi = Cterm {sign=ssign, maxidx=smax, T=propT, t=Bi}
   3.638 +      val ct_Bi = Cterm {sign_ref=ssign_ref, maxidx=smax, T=propT, t=Bi}
   3.639        val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1)
   3.640 -      val (Thm{sign, der, maxidx,shyps,hyps,prop}) = orule
   3.641 +      val (Thm{sign_ref, der, maxidx,shyps,hyps,prop}) = orule
   3.642        val (tpairs,As,B) = Logic.strip_horn prop
   3.643    in  (*no fix_shyps*)
   3.644 -      Thm{sign = merge_thm_sgs(state,orule),
   3.645 +      Thm{sign_ref = merge_thm_sgs(state,orule),
   3.646            der = infer_derivs (Lift_rule(ct_Bi, i), [der]),
   3.647            maxidx = maxidx+smax+1,
   3.648            shyps=union_sort(sshyps,shyps), 
   3.649 @@ -1150,11 +1162,11 @@
   3.650  
   3.651  (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
   3.652  fun assumption i state =
   3.653 -  let val Thm{sign,der,maxidx,hyps,prop,...} = state;
   3.654 +  let val Thm{sign_ref,der,maxidx,hyps,prop,...} = state;
   3.655        val (tpairs, Bs, Bi, C) = dest_state(state,i)
   3.656        fun newth (env as Envir.Envir{maxidx, ...}, tpairs) =
   3.657          fix_shyps [state] (env_codT env)
   3.658 -          (Thm{sign = sign, 
   3.659 +          (Thm{sign_ref = sign_ref, 
   3.660                 der = infer_derivs (Assumption (i, Some env), [der]),
   3.661                 maxidx = maxidx,
   3.662                 shyps = [],
   3.663 @@ -1167,18 +1179,18 @@
   3.664        fun addprfs [] = Sequence.null
   3.665          | addprfs ((t,u)::apairs) = Sequence.seqof (fn()=> Sequence.pull
   3.666               (Sequence.mapp newth
   3.667 -                (Unify.unifiers(sign,Envir.empty maxidx, (t,u)::tpairs))
   3.668 +                (Unify.unifiers(Sign.deref sign_ref,Envir.empty maxidx, (t,u)::tpairs))
   3.669                  (addprfs apairs)))
   3.670    in  addprfs (Logic.assum_pairs Bi)  end;
   3.671  
   3.672  (*Solve subgoal Bi of proof state B1...Bn/C by assumption.
   3.673    Checks if Bi's conclusion is alpha-convertible to one of its assumptions*)
   3.674  fun eq_assumption i state =
   3.675 -  let val Thm{sign,der,maxidx,hyps,prop,...} = state;
   3.676 +  let val Thm{sign_ref,der,maxidx,hyps,prop,...} = state;
   3.677        val (tpairs, Bs, Bi, C) = dest_state(state,i)
   3.678    in  if exists (op aconv) (Logic.assum_pairs Bi)
   3.679        then fix_shyps [state] []
   3.680 -             (Thm{sign = sign, 
   3.681 +             (Thm{sign_ref = sign_ref, 
   3.682                    der = infer_derivs (Assumption (i,None), [der]),
   3.683                    maxidx = maxidx,
   3.684                    shyps = [],
   3.685 @@ -1190,7 +1202,7 @@
   3.686  
   3.687  (*For rotate_tac: fast rotation of assumptions of subgoal i*)
   3.688  fun rotate_rule k i state =
   3.689 -  let val Thm{sign,der,maxidx,hyps,prop,shyps} = state;
   3.690 +  let val Thm{sign_ref,der,maxidx,hyps,prop,shyps} = state;
   3.691        val (tpairs, Bs, Bi, C) = dest_state(state,i)
   3.692        val params = Logic.strip_params Bi
   3.693        and asms   = Logic.strip_assums_hyp Bi
   3.694 @@ -1204,7 +1216,7 @@
   3.695  					       List.take(asms, m),
   3.696  					       concl))
   3.697  		   else raise THM("rotate_rule", m, [state])
   3.698 -  in  Thm{sign = sign, 
   3.699 +  in  Thm{sign_ref = sign_ref, 
   3.700  	  der = infer_derivs (Rotate_rule (k,i), [der]),
   3.701  	  maxidx = maxidx,
   3.702  	  shyps = shyps,
   3.703 @@ -1220,7 +1232,7 @@
   3.704    The names in cs, if distinct, are used for the innermost parameters;
   3.705     preceding parameters may be renamed to make all params distinct.*)
   3.706  fun rename_params_rule (cs, i) state =
   3.707 -  let val Thm{sign,der,maxidx,hyps,...} = state
   3.708 +  let val Thm{sign_ref,der,maxidx,hyps,...} = state
   3.709        val (tpairs, Bs, Bi, C) = dest_state(state,i)
   3.710        val iparams = map #1 (Logic.strip_params Bi)
   3.711        val short = length iparams - length cs
   3.712 @@ -1237,7 +1249,7 @@
   3.713         a::_ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a); 
   3.714  		state)
   3.715       | [] => fix_shyps [state] []
   3.716 -                (Thm{sign = sign,
   3.717 +                (Thm{sign_ref = sign_ref,
   3.718                       der = infer_derivs (Rename_params_rule(cs,i), [der]),
   3.719                       maxidx = maxidx,
   3.720                       shyps = [],
   3.721 @@ -1342,7 +1354,8 @@
   3.722           (*How many hyps to skip over during normalization*)
   3.723       and nlift = Logic.count_prems(strip_all_body Bi,
   3.724                                     if eres_flg then ~1 else 0)
   3.725 -     val sign = merge_thm_sgs(state,orule);
   3.726 +     val sign_ref = merge_thm_sgs(state,orule);
   3.727 +     val sign = Sign.deref sign_ref;
   3.728       (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **)
   3.729       fun addth As ((env as Envir.Envir {maxidx, ...}, tpairs), thq) =
   3.730         let val normt = Envir.norm_term env;
   3.731 @@ -1361,7 +1374,7 @@
   3.732                    (ntps, map normt (Bs @ As), normt C)
   3.733               end
   3.734             val th = (*tuned fix_shyps*)
   3.735 -             Thm{sign = sign,
   3.736 +             Thm{sign_ref = sign_ref,
   3.737                   der = infer_derivs (Bicompose(match, eres_flg,
   3.738                                                 1 + length Bs, nsubgoal, env),
   3.739                                       [rder,sder]),
   3.740 @@ -1452,8 +1465,12 @@
   3.741  fun trace_warning a = if ! trace_simp then warning a else ();
   3.742  fun trace_term a sign t = if ! trace_simp then prtm a sign t else ();
   3.743  fun trace_term_warning a sign t = if ! trace_simp then prtm_warning a sign t else ();
   3.744 -fun trace_thm a (Thm {sign, prop, ...}) = trace_term a sign prop;
   3.745 -fun trace_thm_warning a (Thm {sign, prop, ...}) = trace_term_warning a sign prop;
   3.746 +
   3.747 +fun trace_thm a (Thm {sign_ref, prop, ...}) =
   3.748 +  trace_term a (Sign.deref sign_ref) prop;
   3.749 +
   3.750 +fun trace_thm_warning a (Thm {sign_ref, prop, ...}) =
   3.751 +  trace_term_warning a (Sign.deref sign_ref) prop;
   3.752  
   3.753  
   3.754  
   3.755 @@ -1545,8 +1562,9 @@
   3.756  
   3.757  (* mk_rrule *)
   3.758  
   3.759 -fun mk_rrule (thm as Thm {sign, prop, ...}) =
   3.760 +fun mk_rrule (thm as Thm {sign_ref, prop, ...}) =
   3.761    let
   3.762 +    val sign = Sign.deref sign_ref;
   3.763      val prems = Logic.strip_imp_prems prop;
   3.764      val concl = Logic.strip_imp_concl prop;
   3.765      val (lhs, rhs) = Logic.dest_equals concl handle TERM _ =>
   3.766 @@ -1562,13 +1580,13 @@
   3.767  
   3.768  fun add_simp
   3.769    (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless},
   3.770 -    thm as Thm {sign, prop, ...}) =
   3.771 +    thm as Thm {sign_ref, prop, ...}) =
   3.772    (case mk_rrule thm of
   3.773      None => mss
   3.774    | Some (rrule as {lhs, ...}) =>
   3.775        (trace_thm "Adding rewrite rule:" thm;
   3.776          mk_mss (Net.insert_term ((lhs, rrule), rules, eq_rrule) handle Net.INSERT =>
   3.777 -          (prtm_warning "ignoring duplicate rewrite rule" sign prop; rules),
   3.778 +          (prtm_warning "ignoring duplicate rewrite rule" (Sign.deref sign_ref) prop; rules),
   3.779              congs, procs, bounds, prems, mk_rews, termless)));
   3.780  
   3.781  val add_simps = foldl add_simp;
   3.782 @@ -1580,12 +1598,12 @@
   3.783  
   3.784  fun del_simp
   3.785    (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless},
   3.786 -    thm as Thm {sign, prop, ...}) =
   3.787 +    thm as Thm {sign_ref, prop, ...}) =
   3.788    (case mk_rrule thm of
   3.789      None => mss
   3.790    | Some (rrule as {lhs, ...}) =>
   3.791        mk_mss (Net.delete_term ((lhs, rrule), rules, eq_rrule) handle Net.DELETE =>
   3.792 -        (prtm_warning "rewrite rule not in simpset" sign prop; rules),
   3.793 +        (prtm_warning "rewrite rule not in simpset" (Sign.deref sign_ref) prop; rules),
   3.794            congs, procs, bounds, prems, mk_rews, termless));
   3.795  
   3.796  val del_simps = foldl del_simp;
   3.797 @@ -1628,8 +1646,9 @@
   3.798  (* add_simprocs *)
   3.799  
   3.800  fun add_proc (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless},
   3.801 -    (name, lhs as Cterm {sign, t, ...}, proc, id)) =
   3.802 -  (trace_term ("Adding simplification procedure " ^ name ^ " for:") sign t;
   3.803 +    (name, lhs as Cterm {sign_ref, t, ...}, proc, id)) =
   3.804 +  (trace_term ("Adding simplification procedure " ^ name ^ " for:")
   3.805 +      (Sign.deref sign_ref) t;
   3.806      mk_mss (rules, congs,
   3.807        Net.insert_term ((t, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
   3.808          handle Net.INSERT => (trace_warning "ignored duplicate"; procs),
   3.809 @@ -1690,12 +1709,12 @@
   3.810  *)
   3.811  
   3.812  type prover = meta_simpset -> thm -> thm option;
   3.813 -type termrec = (Sign.sg * term list) * term;
   3.814 +type termrec = (Sign.sg_ref * term list) * term;
   3.815  type conv = meta_simpset -> termrec -> termrec;
   3.816  
   3.817 -fun check_conv (thm as Thm{shyps,hyps,prop,sign,der,maxidx,...}, prop0, ders) =
   3.818 +fun check_conv (thm as Thm{shyps,hyps,prop,sign_ref,der,maxidx,...}, prop0, ders) =
   3.819    let fun err() = (trace_thm "Proved wrong thm (Check subgoaler?)" thm;
   3.820 -                   trace_term "Should have proved" sign prop0;
   3.821 +                   trace_term "Should have proved" (Sign.deref sign_ref) prop0;
   3.822                     None)
   3.823        val (lhs0,_) = Logic.dest_equals(Logic.strip_imp_concl prop0)
   3.824    in case prop of
   3.825 @@ -1722,8 +1741,9 @@
   3.826  
   3.827  (* mk_procrule *)
   3.828  
   3.829 -fun mk_procrule (thm as Thm {sign, prop, ...}) =
   3.830 +fun mk_procrule (thm as Thm {sign_ref, prop, ...}) =
   3.831    let
   3.832 +    val sign = Sign.deref sign_ref;
   3.833      val prems = Logic.strip_imp_prems prop;
   3.834      val concl = Logic.strip_imp_concl prop;
   3.835      val (lhs, _) = Logic.dest_equals concl handle TERM _ =>
   3.836 @@ -1748,15 +1768,17 @@
   3.837      (4) simplification procedures
   3.838  *)
   3.839  
   3.840 -fun rewritec (prover,signt) (mss as Mss{rules, procs, mk_rews, termless, prems, ...}) 
   3.841 +fun rewritec (prover,sign_reft) (mss as Mss{rules, procs, mk_rews, termless, prems, ...}) 
   3.842               (shypst,hypst,maxt,t,ders) =
   3.843    let
   3.844 -      val tsigt = #tsig(Sign.rep_sg signt);
   3.845 -      fun rew {thm as Thm{sign,der,maxidx,shyps,hyps,prop,...}, lhs, perm} =
   3.846 -        let val unit = if Sign.subsig(sign,signt) then ()
   3.847 -                  else (trace_thm_warning "rewrite rule from different theory"
   3.848 -                          thm;
   3.849 -                        raise Pattern.MATCH)
   3.850 +      val signt = Sign.deref sign_reft;
   3.851 +      val tsigt = Sign.tsig_of signt;
   3.852 +      fun rew {thm as Thm{sign_ref,der,maxidx,shyps,hyps,prop,...}, lhs, perm} =
   3.853 +        let
   3.854 +            val _ =
   3.855 +              if Sign.subsig (Sign.deref sign_ref, signt) then ()
   3.856 +              else (trace_thm_warning "rewrite rule from different theory" thm;
   3.857 +                raise Pattern.MATCH);
   3.858              val rprop = if maxt = ~1 then prop
   3.859                          else Logic.incr_indexes([],maxt+1) prop;
   3.860              val rlhs = if maxt = ~1 then lhs
   3.861 @@ -1766,12 +1788,12 @@
   3.862              val hyps' = union_term(hyps,hypst);
   3.863              val shyps' = add_insts_sorts (insts, union_sort(shyps,shypst));
   3.864              val maxidx' = maxidx_of_term prop'
   3.865 -            val ct' = Cterm{sign = signt,       (*used for deriv only*)
   3.866 +            val ct' = Cterm{sign_ref = sign_reft,       (*used for deriv only*)
   3.867                              t = prop',
   3.868                              T = propT,
   3.869                              maxidx = maxidx'}
   3.870              val der' = infer_derivs (RewriteC ct', [der]);
   3.871 -            val thm' = Thm{sign = signt, 
   3.872 +            val thm' = Thm{sign_ref = sign_reft, 
   3.873                             der = der',
   3.874                             shyps = shyps',
   3.875                             hyps = hyps',
   3.876 @@ -1829,11 +1851,12 @@
   3.877  
   3.878  (* conversion to apply a congruence rule to a term *)
   3.879  
   3.880 -fun congc (prover,signt) {thm=cong,lhs=lhs} (shypst,hypst,maxt,t,ders) =
   3.881 -  let val Thm{sign,der,shyps,hyps,maxidx,prop,...} = cong
   3.882 -      val unit = if Sign.subsig(sign,signt) then ()
   3.883 +fun congc (prover,sign_reft) {thm=cong,lhs=lhs} (shypst,hypst,maxt,t,ders) =
   3.884 +  let val signt = Sign.deref sign_reft;
   3.885 +      val tsig = Sign.tsig_of signt;
   3.886 +      val Thm{sign_ref,der,shyps,hyps,maxidx,prop,...} = cong
   3.887 +      val _ = if Sign.subsig(Sign.deref sign_ref,signt) then ()
   3.888                   else error("Congruence rule from different theory")
   3.889 -      val tsig = #tsig(Sign.rep_sg signt)
   3.890        val rprop = if maxt = ~1 then prop
   3.891                    else Logic.incr_indexes([],maxt+1) prop;
   3.892        val rlhs = if maxt = ~1 then lhs
   3.893 @@ -1844,11 +1867,11 @@
   3.894        val prop' = ren_inst(insts,rprop,rlhs,t);
   3.895        val shyps' = add_insts_sorts (insts, union_sort(shyps,shypst))
   3.896        val maxidx' = maxidx_of_term prop'
   3.897 -      val ct' = Cterm{sign = signt,     (*used for deriv only*)
   3.898 +      val ct' = Cterm{sign_ref = sign_reft,     (*used for deriv only*)
   3.899                        t = prop',
   3.900                        T = propT,
   3.901                        maxidx = maxidx'}
   3.902 -      val thm' = Thm{sign = signt, 
   3.903 +      val thm' = Thm{sign_ref = sign_reft, 
   3.904                       der = infer_derivs (CongC ct', [der]),
   3.905                       shyps = shyps',
   3.906                       hyps = union_term(hyps,hypst),
   3.907 @@ -1865,15 +1888,15 @@
   3.908  
   3.909  
   3.910  
   3.911 -fun bottomc ((simprem,useprem),prover,sign) =
   3.912 +fun bottomc ((simprem,useprem),prover,sign_ref) =
   3.913   let fun botc fail mss trec =
   3.914            (case subc mss trec of
   3.915               some as Some(trec1) =>
   3.916 -               (case rewritec (prover,sign) mss trec1 of
   3.917 +               (case rewritec (prover,sign_ref) mss trec1 of
   3.918                    Some(trec2) => botc false mss trec2
   3.919                  | None => some)
   3.920             | None =>
   3.921 -               (case rewritec (prover,sign) mss trec of
   3.922 +               (case rewritec (prover,sign_ref) mss trec of
   3.923                    Some(trec2) => botc false mss trec2
   3.924                  | None => if fail then None else Some(trec)))
   3.925  
   3.926 @@ -1926,7 +1949,7 @@
   3.927                      Const(a,_) =>
   3.928                        (case assoc_string(congs,a) of
   3.929                           None => appc()
   3.930 -                       | Some(cong) => (congc (prover mss,sign) cong trec
   3.931 +                       | Some(cong) => (congc (prover mss,sign_ref) cong trec
   3.932                                          handle Pattern.MATCH => appc() ) )
   3.933                    | _ => appc()
   3.934                 end)
   3.935 @@ -1941,8 +1964,8 @@
   3.936               if not useprem then mss else
   3.937               if maxidx1 <> ~1 then (trace_term_warning
   3.938  "Cannot add premise as rewrite rule because it contains (type) unknowns:"
   3.939 -                                                  sign s1; mss)
   3.940 -             else let val thm = assume (Cterm{sign=sign, t=s1, 
   3.941 +                                                  (Sign.deref sign_ref) s1; mss)
   3.942 +             else let val thm = assume (Cterm{sign_ref=sign_ref, t=s1, 
   3.943                                                T=propT, maxidx=maxidx1})
   3.944                    in add_simps(add_prems(mss,[thm]), mk_rews thm) end
   3.945             val (shyps2,hyps2,maxidx2,u1,ders2) = 
   3.946 @@ -1968,19 +1991,19 @@
   3.947  (* FIXME: check that #bounds(mss) does not "occur" in ct alread *)
   3.948  
   3.949  fun rewrite_cterm mode mss prover ct =
   3.950 -  let val {sign, t, T, maxidx} = rep_cterm ct;
   3.951 +  let val Cterm {sign_ref, t, T, maxidx} = ct;
   3.952        val (shyps,hyps,maxu,u,ders) =
   3.953 -        bottomc (mode,prover,sign) mss 
   3.954 +        bottomc (mode,prover, sign_ref) mss 
   3.955                  (add_term_sorts(t,[]), [], maxidx, t, []);
   3.956        val prop = Logic.mk_equals(t,u)
   3.957    in
   3.958 -      Thm{sign = sign, 
   3.959 +      Thm{sign_ref = sign_ref, 
   3.960            der = infer_derivs (Rewrite_cterm ct, ders),
   3.961            maxidx = Int.max (maxidx,maxu),
   3.962            shyps = shyps, 
   3.963            hyps = hyps, 
   3.964            prop = prop}
   3.965 -  end
   3.966 +  end;
   3.967  
   3.968  
   3.969  
   3.970 @@ -1997,13 +2020,14 @@
   3.971    in
   3.972      fn (sign, exn) =>
   3.973        let
   3.974 -        val sign' = Sign.merge (sg, sign);
   3.975 +        val sign_ref' = Sign.merge_refs (Sign.self_ref sg, Sign.self_ref sign);
   3.976 +        val sign' = Sign.deref sign_ref';
   3.977          val (prop, T, maxidx) = Sign.certify_term sign' (oracle (sign', exn));
   3.978        in
   3.979          if T <> propT then
   3.980            raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
   3.981          else fix_shyps [] []
   3.982 -          (Thm {sign = sign', 
   3.983 +          (Thm {sign_ref = sign_ref', 
   3.984              der = Join (Oracle (thy, name, sign, exn), []),
   3.985              maxidx = maxidx,
   3.986              shyps = [],