src/Pure/Isar/locale.ML
changeset 16458 4c6fd0c01d28
parent 16346 baa7b5324fc1
child 16620 2a7f46324218
     1.1 --- a/src/Pure/Isar/locale.ML	Fri Jun 17 18:33:42 2005 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Fri Jun 17 18:35:27 2005 +0200
     1.3 @@ -44,8 +44,8 @@
     1.4    type element
     1.5    type element_i
     1.6    type locale
     1.7 -  val intern: Sign.sg -> xstring -> string
     1.8 -  val extern: Sign.sg -> string -> xstring
     1.9 +  val intern: theory -> xstring -> string
    1.10 +  val extern: theory -> string -> xstring
    1.11    val the_locale: theory -> string -> locale
    1.12    val intern_attrib_elem: theory ->
    1.13      ('typ, 'term, 'fact) elem -> ('typ, 'term, 'fact) elem
    1.14 @@ -161,11 +161,11 @@
    1.15        then t
    1.16        else Term.map_term_types (tinst_tab_type tinst) t;
    1.17  
    1.18 -fun tinst_tab_thm sg tinst thm = if Symtab.is_empty tinst
    1.19 +fun tinst_tab_thm thy tinst thm = if Symtab.is_empty tinst
    1.20        then thm
    1.21        else let
    1.22 -          val cert = Thm.cterm_of sg;
    1.23 -          val certT = Thm.ctyp_of sg;
    1.24 +          val cert = Thm.cterm_of thy;
    1.25 +          val certT = Thm.ctyp_of thy;
    1.26            val {hyps, prop, ...} = Thm.rep_thm thm;
    1.27            val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
    1.28            val tinst' = Symtab.dest tinst |>
    1.29 @@ -198,11 +198,11 @@
    1.30              | instf (s $ t) = instf s $ instf t
    1.31          in instf end;
    1.32  
    1.33 -fun inst_tab_thm sg (inst, tinst) thm = if Symtab.is_empty inst
    1.34 -      then tinst_tab_thm sg tinst thm
    1.35 +fun inst_tab_thm thy (inst, tinst) thm = if Symtab.is_empty inst
    1.36 +      then tinst_tab_thm thy tinst thm
    1.37        else let
    1.38 -          val cert = Thm.cterm_of sg;
    1.39 -          val certT = Thm.ctyp_of sg;
    1.40 +          val cert = Thm.cterm_of thy;
    1.41 +          val certT = Thm.ctyp_of thy;
    1.42            val {hyps, prop, ...} = Thm.rep_thm thm;
    1.43            (* type instantiations *)
    1.44            val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
    1.45 @@ -218,7 +218,7 @@
    1.46                      if a = x then SOME (Free (x, tinst_tab_type tinst T), t)
    1.47                      else NONE) frees);
    1.48          in
    1.49 -          if null tinst' andalso null inst' then tinst_tab_thm sg tinst thm
    1.50 +          if null tinst' andalso null inst' then tinst_tab_thm thy tinst thm
    1.51            else thm |> Drule.implies_intr_list (map cert hyps)
    1.52              |> Drule.tvars_intr_list (map #1 tinst')
    1.53              |> (fn (th, al) => th |> Thm.instantiate
    1.54 @@ -239,9 +239,9 @@
    1.55      val empty: T
    1.56      val join: T * T -> T
    1.57      val dest: T -> (term list * ((string * Attrib.src list) * thm list)) list
    1.58 -    val lookup: Sign.sg -> T * term list ->
    1.59 +    val lookup: theory -> T * term list ->
    1.60        ((string * Attrib.src list) * thm list) option
    1.61 -    val insert: Sign.sg -> term list * (string * Attrib.src list) -> T ->
    1.62 +    val insert: theory -> term list * (string * Attrib.src list) -> T ->
    1.63        T * (term list * ((string * Attrib.src list) * thm list)) list
    1.64      val add_witness: term list -> thm -> T -> T
    1.65    end =
    1.66 @@ -262,7 +262,7 @@
    1.67  
    1.68    (* joining of registrations: prefix and attributs of left theory,
    1.69       thms are equal, no attempt to subsumption testing *)
    1.70 -  fun join (r1, r2) = Termtab.join (fn (reg, _) => SOME reg) (r1, r2);
    1.71 +  fun join (r1, r2) = Termtab.join (fn _ => fn (reg, _) => SOME reg) (r1, r2);
    1.72  
    1.73    fun dest regs = map (apfst untermify) (Termtab.dest regs);
    1.74  
    1.75 @@ -321,8 +321,8 @@
    1.76  
    1.77  (** theory data **)
    1.78  
    1.79 -structure GlobalLocalesArgs =
    1.80 -struct
    1.81 +structure GlobalLocalesData = TheoryDataFun
    1.82 +(struct
    1.83    val name = "Isar/locales";
    1.84    type T = NameSpace.T * locale Symtab.table * Registrations.T Symtab.table;
    1.85      (* 1st entry: locale namespace,
    1.86 @@ -331,39 +331,37 @@
    1.87  
    1.88    val empty = (NameSpace.empty, Symtab.empty, Symtab.empty);
    1.89    val copy = I;
    1.90 -  val prep_ext = I;
    1.91 +  val extend = I;
    1.92  
    1.93 -  fun join_locs ({predicate, import, elems, params}: locale,
    1.94 +  fun join_locs _ ({predicate, import, elems, params}: locale,
    1.95        {elems = elems', ...}: locale) =
    1.96      SOME {predicate = predicate, import = import,
    1.97        elems = gen_merge_lists eq_snd elems elems',
    1.98        params = params};
    1.99 -  fun merge ((space1, locs1, regs1), (space2, locs2, regs2)) =
   1.100 +  fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
   1.101      (NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2),
   1.102 -     Symtab.join (SOME o Registrations.join) (regs1, regs2));
   1.103 +     Symtab.join (K (SOME o Registrations.join)) (regs1, regs2));
   1.104  
   1.105    fun print _ (space, locs, _) =
   1.106      Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
   1.107      |> Pretty.writeln;
   1.108 -end;
   1.109 +end);
   1.110  
   1.111 -structure GlobalLocalesData = TheoryDataFun(GlobalLocalesArgs);
   1.112  val _ = Context.add_setup [GlobalLocalesData.init];
   1.113  
   1.114  
   1.115  
   1.116  (** context data **)
   1.117  
   1.118 -structure LocalLocalesArgs =
   1.119 -struct
   1.120 +structure LocalLocalesData = ProofDataFun
   1.121 +(struct
   1.122    val name = "Isar/locales";
   1.123    type T = Registrations.T Symtab.table;
   1.124      (* registrations, indexed by locale name *)
   1.125    fun init _ = Symtab.empty;
   1.126    fun print _ _ = ();
   1.127 -end;
   1.128 +end);
   1.129  
   1.130 -structure LocalLocalesData = ProofDataFun(LocalLocalesArgs);
   1.131  val _ = Context.add_setup [LocalLocalesData.init];
   1.132  
   1.133  
   1.134 @@ -371,12 +369,12 @@
   1.135  
   1.136  val print_locales = GlobalLocalesData.print;
   1.137  
   1.138 -val intern = NameSpace.intern o #1 o GlobalLocalesData.get_sg;
   1.139 -val extern = NameSpace.extern o #1 o GlobalLocalesData.get_sg;
   1.140 +val intern = NameSpace.intern o #1 o GlobalLocalesData.get;
   1.141 +val extern = NameSpace.extern o #1 o GlobalLocalesData.get;
   1.142  
   1.143  fun declare_locale name thy =
   1.144    thy |> GlobalLocalesData.map (fn (space, locs, regs) =>
   1.145 -    (Sign.declare_name (Theory.sign_of thy) name space, locs, regs));
   1.146 +    (Sign.declare_name thy name space, locs, regs));
   1.147  
   1.148  fun put_locale name loc =
   1.149    GlobalLocalesData.map (fn (space, locs, regs) =>
   1.150 @@ -408,15 +406,15 @@
   1.151  val get_local_registrations =
   1.152       gen_get_registrations LocalLocalesData.get;
   1.153  
   1.154 -fun gen_get_registration get get_sg thy_ctxt (name, ps) =
   1.155 +fun gen_get_registration get thy_of thy_ctxt (name, ps) =
   1.156    case Symtab.lookup (get thy_ctxt, name) of
   1.157        NONE => NONE
   1.158 -    | SOME reg => Registrations.lookup (get_sg thy_ctxt) (reg, ps);
   1.159 +    | SOME reg => Registrations.lookup (thy_of thy_ctxt) (reg, ps);
   1.160  
   1.161  val get_global_registration =
   1.162 -     gen_get_registration (#3 o GlobalLocalesData.get) Theory.sign_of;
   1.163 +     gen_get_registration (#3 o GlobalLocalesData.get) I;
   1.164  val get_local_registration =
   1.165 -     gen_get_registration LocalLocalesData.get ProofContext.sign_of;
   1.166 +     gen_get_registration LocalLocalesData.get ProofContext.theory_of;
   1.167  
   1.168  val test_global_registration = isSome oo get_global_registration;
   1.169  val test_local_registration = isSome oo get_local_registration;
   1.170 @@ -430,15 +428,15 @@
   1.171  
   1.172  (* add registration to theory or context, ignored if subsumed *)
   1.173  
   1.174 -fun gen_put_registration map_data get_sg (name, ps) attn thy_ctxt =
   1.175 +fun gen_put_registration map_data thy_of (name, ps) attn thy_ctxt =
   1.176    map_data (fn regs =>
   1.177      let
   1.178 -      val sg = get_sg thy_ctxt;
   1.179 +      val thy = thy_of thy_ctxt;
   1.180        val reg = getOpt (Symtab.lookup (regs, name), Registrations.empty);
   1.181 -      val (reg', sups) = Registrations.insert sg (ps, attn) reg;
   1.182 +      val (reg', sups) = Registrations.insert thy (ps, attn) reg;
   1.183        val _ = if not (null sups) then warning
   1.184                  ("Subsumed interpretation(s) of locale " ^
   1.185 -                 quote (extern sg name) ^
   1.186 +                 quote (extern thy name) ^
   1.187                   "\nby interpretation(s) with the following prefix(es):\n" ^
   1.188                    commas_quote (map (fn (_, ((s, _), _)) => s) sups))
   1.189                else ();
   1.190 @@ -446,10 +444,9 @@
   1.191  
   1.192  val put_global_registration =
   1.193       gen_put_registration (fn f =>
   1.194 -       GlobalLocalesData.map (fn (space, locs, regs) =>
   1.195 -         (space, locs, f regs))) Theory.sign_of;
   1.196 +       GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, f regs))) I;
   1.197  val put_local_registration =
   1.198 -     gen_put_registration LocalLocalesData.map ProofContext.sign_of;
   1.199 +     gen_put_registration LocalLocalesData.map ProofContext.theory_of;
   1.200  
   1.201  (* TODO: needed? *)
   1.202  (*
   1.203 @@ -487,7 +484,6 @@
   1.204  
   1.205  fun imports thy (upper, lower) =
   1.206    let
   1.207 -    val sign = sign_of thy;
   1.208      fun imps (Locale name) low = (name = low) orelse
   1.209        (case get_locale thy name of
   1.210             NONE => false
   1.211 @@ -495,7 +491,7 @@
   1.212        | imps (Rename (expr, _)) low = imps expr low
   1.213        | imps (Merge es) low = exists (fn e => imps e low) es;
   1.214    in
   1.215 -    imps (Locale (intern sign upper)) (intern sign lower)
   1.216 +    imps (Locale (intern thy upper)) (intern thy lower)
   1.217    end;
   1.218  
   1.219  
   1.220 @@ -505,7 +501,6 @@
   1.221    let
   1.222      val ctxt = mk_ctxt thy_ctxt;
   1.223      val thy = ProofContext.theory_of ctxt;
   1.224 -    val sg = Theory.sign_of thy;
   1.225  
   1.226      val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
   1.227      val prt_atts = Args.pretty_attribs ctxt;
   1.228 @@ -517,7 +512,7 @@
   1.229                [Pretty.str ":", Pretty.brk 1,
   1.230                  Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts))]));
   1.231  
   1.232 -    val loc_int = intern sg loc;
   1.233 +    val loc_int = intern thy loc;
   1.234      val regs = get_regs thy_ctxt;
   1.235      val loc_regs = Symtab.lookup (regs, loc_int);
   1.236    in
   1.237 @@ -547,9 +542,9 @@
   1.238  
   1.239  fun err_in_locale ctxt msg ids =
   1.240    let
   1.241 -    val sign = ProofContext.sign_of ctxt;
   1.242 +    val thy = ProofContext.theory_of ctxt;
   1.243      fun prt_id (name, parms) =
   1.244 -      [Pretty.block (Pretty.breaks (map Pretty.str (extern sign name :: parms)))];
   1.245 +      [Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))];
   1.246      val prt_ids = List.concat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids));
   1.247      val err_msg =
   1.248        if forall (equal "" o #1) ids then msg
   1.249 @@ -591,7 +586,7 @@
   1.250  
   1.251  fun map_attrib_elem f = map_elem {name = I, var = I, typ = I, term = I, fact = I, attrib = f};
   1.252  
   1.253 -fun intern_attrib_elem thy = map_attrib_elem (Attrib.intern_src (Theory.sign_of thy));
   1.254 +fun intern_attrib_elem thy = map_attrib_elem (Attrib.intern_src thy);
   1.255  
   1.256  fun intern_attrib_elem_expr thy (Elem elem) = Elem (intern_attrib_elem thy elem)
   1.257    | intern_attrib_elem_expr _ (Expr expr) = Expr expr;
   1.258 @@ -623,8 +618,8 @@
   1.259  
   1.260  fun rename_thm ren th =
   1.261    let
   1.262 -    val {sign, hyps, prop, maxidx, ...} = Thm.rep_thm th;
   1.263 -    val cert = Thm.cterm_of sign;
   1.264 +    val {thy, hyps, prop, maxidx, ...} = Thm.rep_thm th;
   1.265 +    val cert = Thm.cterm_of thy;
   1.266      val (xs, Ts) = Library.split_list (Library.foldl Term.add_frees ([], prop :: hyps));
   1.267      val xs' = map (rename ren) xs;
   1.268      fun cert_frees names = map (cert o Free) (names ~~ Ts);
   1.269 @@ -659,9 +654,9 @@
   1.270  fun inst_thm _ [] th = th
   1.271    | inst_thm ctxt env th =
   1.272        let
   1.273 -        val sign = ProofContext.sign_of ctxt;
   1.274 -        val cert = Thm.cterm_of sign;
   1.275 -        val certT = Thm.ctyp_of sign;
   1.276 +        val thy = ProofContext.theory_of ctxt;
   1.277 +        val cert = Thm.cterm_of thy;
   1.278 +        val certT = Thm.ctyp_of thy;
   1.279          val {hyps, prop, maxidx, ...} = Thm.rep_thm th;
   1.280          val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
   1.281          val env' = List.filter (fn ((a, _), _) => a mem_string tfrees) env;
   1.282 @@ -686,16 +681,16 @@
   1.283  
   1.284  (* instantiate TFrees *)
   1.285  
   1.286 -fun tinst_tab_elem sg tinst =
   1.287 -  map_values (tinst_tab_type tinst) (tinst_tab_term tinst) (tinst_tab_thm sg tinst);
   1.288 +fun tinst_tab_elem thy tinst =
   1.289 +  map_values (tinst_tab_type tinst) (tinst_tab_term tinst) (tinst_tab_thm thy tinst);
   1.290  
   1.291  (* instantiate TFrees and Frees *)
   1.292  
   1.293 -fun inst_tab_elem sg (inst as (_, tinst)) =
   1.294 -  map_values (tinst_tab_type tinst) (inst_tab_term inst) (inst_tab_thm sg inst);
   1.295 +fun inst_tab_elem thy (inst as (_, tinst)) =
   1.296 +  map_values (tinst_tab_type tinst) (inst_tab_term inst) (inst_tab_thm thy inst);
   1.297  
   1.298 -fun inst_tab_elems sign inst ((n, ps), elems) =
   1.299 -      ((n, map (inst_tab_term inst) ps), map (inst_tab_elem sign inst) elems);
   1.300 +fun inst_tab_elems thy inst ((n, ps), elems) =
   1.301 +      ((n, map (inst_tab_term inst) ps), map (inst_tab_elem thy inst) elems);
   1.302  
   1.303  
   1.304  (** structured contexts: rename + merge + implicit type instantiation **)
   1.305 @@ -719,7 +714,7 @@
   1.306  
   1.307      val (maxidx', Ts') = foldl_map paramify (maxidx, Ts);
   1.308      val (maxidx'', Us') = foldl_map paramify (maxidx', Us);
   1.309 -    val tsig = Sign.tsig_of (ProofContext.sign_of ctxt);
   1.310 +    val tsig = Sign.tsig_of (ProofContext.theory_of ctxt);
   1.311  
   1.312      fun unify (env, (SOME T, SOME U)) = (Type.unify tsig env (U, T)
   1.313            handle Type.TUNIFY =>
   1.314 @@ -771,8 +766,8 @@
   1.315  fun unify_parms ctxt (fixed_parms : (string * typ) list)
   1.316    (raw_parmss : (string * typ option) list list) =
   1.317    let
   1.318 -    val sign = ProofContext.sign_of ctxt;
   1.319 -    val tsig = Sign.tsig_of sign;
   1.320 +    val thy = ProofContext.theory_of ctxt;
   1.321 +    val tsig = Sign.tsig_of thy;
   1.322      val maxidx = length raw_parmss;
   1.323      val idx_parmss = (0 upto maxidx - 1) ~~ raw_parmss;
   1.324  
   1.325 @@ -783,7 +778,7 @@
   1.326      fun unify T ((env, maxidx), U) =
   1.327        Type.unify tsig (env, maxidx) (U, T)
   1.328        handle Type.TUNIFY =>
   1.329 -        let val prt = Sign.string_of_typ sign
   1.330 +        let val prt = Sign.string_of_typ thy
   1.331          in raise TYPE ("unify_parms: failed to unify types " ^
   1.332            prt U ^ " and " ^ prt T, [U, T], [])
   1.333          end
   1.334 @@ -1065,9 +1060,9 @@
   1.335  
   1.336  (* expressions *)
   1.337  
   1.338 -fun intern_expr sg (Locale xname) = Locale (intern sg xname)
   1.339 -  | intern_expr sg (Merge exprs) = Merge (map (intern_expr sg) exprs)
   1.340 -  | intern_expr sg (Rename (expr, xs)) = Rename (intern_expr sg expr, xs);
   1.341 +fun intern_expr thy (Locale xname) = Locale (intern thy xname)
   1.342 +  | intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs)
   1.343 +  | intern_expr thy (Rename (expr, xs)) = Rename (intern_expr thy expr, xs);
   1.344  
   1.345  
   1.346  (* parameters *)
   1.347 @@ -1196,14 +1191,14 @@
   1.348      val eq' = Term.list_abs_free (map Term.dest_Free xs, rhs);
   1.349    in (Term.dest_Free f, eq') end;
   1.350  
   1.351 -fun abstract_thm sign eq =
   1.352 -  Thm.assume (Thm.cterm_of sign eq) |> Drule.gen_all |> Drule.abs_def;
   1.353 +fun abstract_thm thy eq =
   1.354 +  Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;
   1.355  
   1.356  fun bind_def ctxt (name, ps) ((xs, env, ths), eq) =
   1.357    let
   1.358      val ((y, T), b) = abstract_term eq;
   1.359      val b' = norm_term env b;
   1.360 -    val th = abstract_thm (ProofContext.sign_of ctxt) eq;
   1.361 +    val th = abstract_thm (ProofContext.theory_of ctxt) eq;
   1.362      fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];
   1.363    in
   1.364      conditional (exists (equal y o #1) xs) (fn () =>
   1.365 @@ -1382,7 +1377,7 @@
   1.366       {var = I, typ = I, term = I,
   1.367        name = prep_name ctxt,
   1.368        fact = get ctxt,
   1.369 -      attrib = Args.assignable o intern (ProofContext.sign_of ctxt)};
   1.370 +      attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
   1.371  
   1.372  in
   1.373  
   1.374 @@ -1399,11 +1394,12 @@
   1.375  fun prep_context_statement prep_expr prep_elemss prep_facts
   1.376      do_close fixed_params import elements raw_concl context =
   1.377    let
   1.378 -    val sign = ProofContext.sign_of context;
   1.379 +    val thy = ProofContext.theory_of context;
   1.380  
   1.381 -    val ((import_ids, import_syn), raw_import_elemss) = flatten (context, prep_expr sign) (([], Symtab.empty), Expr import);
   1.382 +    val ((import_ids, import_syn), raw_import_elemss) =
   1.383 +      flatten (context, prep_expr thy) (([], Symtab.empty), Expr import);
   1.384      (* CB: normalise "includes" among elements *)
   1.385 -    val ((ids, syn), raw_elemsss) = foldl_map (flatten (context, prep_expr sign))
   1.386 +    val ((ids, syn), raw_elemsss) = foldl_map (flatten (context, prep_expr thy))
   1.387        ((import_ids, import_syn), elements);
   1.388  
   1.389      val raw_elemss = List.concat raw_elemsss;
   1.390 @@ -1426,7 +1422,7 @@
   1.391      val stmt = gen_distinct Term.aconv
   1.392         (List.concat (map (fn ((_, axs), _) =>
   1.393           List.concat (map (#hyps o Thm.rep_thm) axs)) qs));
   1.394 -    val cstmt = map (cterm_of sign) stmt;
   1.395 +    val cstmt = map (cterm_of thy) stmt;
   1.396    in
   1.397      ((((import_ctxt, import_elemss), (ctxt, elemss, syn)), (parms, spec, defs)), (cstmt, concl))
   1.398    end;
   1.399 @@ -1437,7 +1433,7 @@
   1.400  fun gen_statement prep_locale prep_ctxt raw_locale elems concl ctxt =
   1.401    let
   1.402      val thy = ProofContext.theory_of ctxt;
   1.403 -    val locale = Option.map (prep_locale (Theory.sign_of thy)) raw_locale;
   1.404 +    val locale = Option.map (prep_locale thy) raw_locale;
   1.405      val (target_stmt, fixed_params, import) =
   1.406        (case locale of NONE => ([], [], empty)
   1.407        | SOME name =>
   1.408 @@ -1577,7 +1573,7 @@
   1.409      val (parms, parmTs_o) =
   1.410            the_locale thy target |> #params |> fst |> map fst |> split_list;
   1.411      val parmvTs = map (Type.varifyT o valOf) parmTs_o;
   1.412 -    val ids = flatten (ProofContext.init thy, intern_expr (Theory.sign_of thy))
   1.413 +    val ids = flatten (ProofContext.init thy, intern_expr thy)
   1.414        (([], Symtab.empty), Expr (Locale target)) |> fst |> fst |> map fst;
   1.415  
   1.416      val regs = get_global_registrations thy target;
   1.417 @@ -1586,10 +1582,9 @@
   1.418  
   1.419      fun activate (thy, (vts, ((prfx, atts2), _))) =
   1.420        let
   1.421 -        val sg = Theory.sign_of thy;
   1.422          val ts = map Logic.unvarify vts;
   1.423          (* type instantiation *)
   1.424 -        val vtinst = Library.foldl (Type.typ_match (Sign.tsig_of sg))
   1.425 +        val vtinst = Library.foldl (Type.typ_match (Sign.tsig_of thy))
   1.426               (Vartab.empty, (parmvTs ~~ map Term.fastype_of ts));
   1.427          val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T))
   1.428               |> Symtab.make;            
   1.429 @@ -1602,7 +1597,7 @@
   1.430          val args' = map (fn ((n, atts), [(ths, [])]) =>
   1.431              ((if prfx = "" orelse n = "" then "" else NameSpace.pack [prfx, n],  (* FIXME *)
   1.432                map (Attrib.global_attribute_i thy) (atts @ atts2)),
   1.433 -             [(map (Drule.standard o Drule.satisfy_hyps prems o inst_tab_thm sg (inst, tinst)) ths, [])]))
   1.434 +             [(map (Drule.standard o Drule.satisfy_hyps prems o inst_tab_thm thy (inst, tinst)) ths, [])]))
   1.435            args;
   1.436        in global_note_accesses_i (Drule.kind kind) prfx args' thy |> fst end;
   1.437    in Library.foldl activate (thy, regs) end;
   1.438 @@ -1632,7 +1627,7 @@
   1.439  fun gen_note_thmss prep_locale prep_facts kind raw_loc args thy =
   1.440    let
   1.441      val thy_ctxt = ProofContext.init thy;
   1.442 -    val loc = prep_locale (Theory.sign_of thy) raw_loc;
   1.443 +    val loc = prep_locale thy raw_loc;
   1.444      val (_, (stmt, _), loc_ctxt, _, _) = cert_context_statement (SOME loc) [] [] thy_ctxt;
   1.445      val export = ProofContext.export_standard stmt loc_ctxt thy_ctxt;
   1.446  
   1.447 @@ -1678,14 +1673,14 @@
   1.448  val introN = "intro";
   1.449  val axiomsN = "axioms";
   1.450  
   1.451 -fun atomize_spec sign ts =
   1.452 +fun atomize_spec thy ts =
   1.453    let
   1.454      val t = foldr1 Logic.mk_conjunction ts;
   1.455 -    val body = ObjectLogic.atomize_term sign t;
   1.456 +    val body = ObjectLogic.atomize_term thy t;
   1.457      val bodyT = Term.fastype_of body;
   1.458    in
   1.459 -    if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of sign t))
   1.460 -    else (body, bodyT, ObjectLogic.atomize_rule sign (Thm.cterm_of sign t))
   1.461 +    if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
   1.462 +    else (body, bodyT, ObjectLogic.atomize_rule thy (Thm.cterm_of thy t))
   1.463    end;
   1.464  
   1.465  fun aprop_tr' n c = (c, fn args =>
   1.466 @@ -1703,10 +1698,9 @@
   1.467  
   1.468  fun def_pred bname parms defs ts norm_ts thy =
   1.469    let
   1.470 -    val sign = Theory.sign_of thy;
   1.471 -    val name = Sign.full_name sign bname;
   1.472 +    val name = Sign.full_name thy bname;
   1.473  
   1.474 -    val (body, bodyT, body_eq) = atomize_spec sign norm_ts;
   1.475 +    val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
   1.476      val env = Term.add_term_free_names (body, []);
   1.477      val xs = List.filter (fn (x, _) => x mem_string env) parms;
   1.478      val Ts = map #2 xs;
   1.479 @@ -1716,7 +1710,7 @@
   1.480  
   1.481      val args = map Logic.mk_type extraTs @ map Free xs;
   1.482      val head = Term.list_comb (Const (name, predT), args);
   1.483 -    val statement = ObjectLogic.assert_propT sign head;
   1.484 +    val statement = ObjectLogic.assert_propT thy head;
   1.485  
   1.486      val (defs_thy, [pred_def]) =
   1.487        thy
   1.488 @@ -1725,10 +1719,9 @@
   1.489        |> Theory.add_consts_i [(bname, predT, Syntax.NoSyn)]
   1.490        |> PureThy.add_defs_i false [((Thm.def_name bname, Logic.mk_equals (head, body)), [])];
   1.491  
   1.492 -    val defs_sign = Theory.sign_of defs_thy;
   1.493 -    val cert = Thm.cterm_of defs_sign;
   1.494 +    val cert = Thm.cterm_of defs_thy;
   1.495  
   1.496 -    val intro = Tactic.prove_standard defs_sign [] norm_ts statement (fn _ =>
   1.497 +    val intro = Tactic.prove_standard defs_thy [] norm_ts statement (fn _ =>
   1.498        Tactic.rewrite_goals_tac [pred_def] THEN
   1.499        Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
   1.500        Tactic.compose_tac (false, Drule.conj_intr_list (map (Thm.assume o cert) norm_ts), 0) 1);
   1.501 @@ -1738,7 +1731,7 @@
   1.502          Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))]
   1.503        |> Drule.conj_elim_precise (length ts);
   1.504      val axioms = (ts ~~ conjuncts) |> map (fn (t, ax) =>
   1.505 -      Tactic.prove_plain defs_sign [] [] t (fn _ =>
   1.506 +      Tactic.prove_plain defs_thy [] [] t (fn _ =>
   1.507          Tactic.rewrite_goals_tac defs THEN
   1.508          Tactic.compose_tac (false, ax, 0) 1));
   1.509    in (defs_thy, (statement, intro, axioms)) end;
   1.510 @@ -1788,7 +1781,7 @@
   1.511          let
   1.512            val (def_thy, (statement, intro, axioms)) =
   1.513              thy' |> def_pred bname parms defs (ints @ more_ts) (ints' @ more_ts);
   1.514 -          val cstatement = Thm.cterm_of (Theory.sign_of def_thy) statement;
   1.515 +          val cstatement = Thm.cterm_of def_thy statement;
   1.516          in
   1.517            def_thy |> note_thmss_qualified "" bname
   1.518              [((introN, []), [([intro], [])]),
   1.519 @@ -1808,8 +1801,7 @@
   1.520    (* CB: do_pred controls generation of predicates.
   1.521           true -> with, false -> without predicates. *)
   1.522    let
   1.523 -    val sign = Theory.sign_of thy;
   1.524 -    val name = Sign.full_name sign bname;
   1.525 +    val name = Sign.full_name thy bname;
   1.526      val _ = conditional (isSome (get_locale thy name)) (fn () =>
   1.527        error ("Duplicate definition of locale " ^ quote name));
   1.528  
   1.529 @@ -1817,6 +1809,7 @@
   1.530      val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)), text) =
   1.531        prep_ctxt raw_import raw_body thy_ctxt;
   1.532      val elemss = import_elemss @ body_elemss;
   1.533 +    val import = prep_expr thy raw_import;
   1.534  
   1.535      val (pred_thy, (elemss', predicate as (predicate_statement, predicate_axioms))) =
   1.536        if do_pred then thy |> define_preds bname text elemss
   1.537 @@ -1838,7 +1831,7 @@
   1.538      pred_thy
   1.539      |> note_thmss_qualified "" name facts' |> #1
   1.540      |> declare_locale name
   1.541 -    |> put_locale name {predicate = predicate, import = prep_expr sign raw_import,
   1.542 +    |> put_locale name {predicate = predicate, import = import,
   1.543          elems = map (fn e => (e, stamp ())) (List.concat (map #2 (List.filter (equal "" o #1 o #1) elemss'))),
   1.544          params = (params_of elemss' |>
   1.545            map (fn (x, T) => ((x, T), valOf (Symtab.lookup (syn, x)))), map #1 (params_of body_elemss))}
   1.546 @@ -1935,10 +1928,10 @@
   1.547      attn expr insts thy_ctxt =
   1.548    let
   1.549      val ctxt = mk_ctxt thy_ctxt;
   1.550 -    val sign = ProofContext.sign_of ctxt;
   1.551 +    val thy = ProofContext.theory_of ctxt;
   1.552  
   1.553      val ctxt' = ctxt |> ProofContext.theory_of |> ProofContext.init;
   1.554 -    val ((ids, _), raw_elemss) = flatten (ctxt', intern_expr sign)
   1.555 +    val ((ids, _), raw_elemss) = flatten (ctxt', intern_expr thy)
   1.556            (([], Symtab.empty), Expr expr);
   1.557      val do_close = false;  (* effect unknown *)
   1.558      val ((parms, all_elemss, _), (spec, (xs, defs, _))) =
   1.559 @@ -2004,7 +1997,7 @@
   1.560  
   1.561      (* instantiate ids and elements *)
   1.562      val inst_elemss = map
   1.563 -          (fn (id, (_, elems)) => inst_tab_elems sign (inst, tinst) (id, 
   1.564 +          (fn (id, (_, elems)) => inst_tab_elems thy (inst, tinst) (id, 
   1.565              map (fn Int e => e) elems)) 
   1.566            (ids' ~~ all_elemss);
   1.567  
   1.568 @@ -2016,7 +2009,7 @@
   1.569      val propss = extract_asms_elemss new_inst_elemss;
   1.570  
   1.571      val bind_attrib = Attrib.crude_closure ctxt o Args.assignable;
   1.572 -    val attn' = apsnd (map (bind_attrib o Attrib.intern_src sign)) attn;
   1.573 +    val attn' = apsnd (map (bind_attrib o Attrib.intern_src thy)) attn;
   1.574  
   1.575      (** add registrations to theory or context,
   1.576          without theorems, these are added after the proof **)
   1.577 @@ -2034,7 +2027,7 @@
   1.578  val prep_global_registration = gen_prep_registration
   1.579       ProofContext.init false
   1.580       (fn thy => fn sorts => fn used =>
   1.581 -       Sign.read_def_terms (Theory.sign_of thy, K NONE, sorts) used true)
   1.582 +       Sign.read_def_terms (thy, K NONE, sorts) used true)
   1.583       (fn thy => fn (name, ps) =>
   1.584         test_global_registration thy (name, map Logic.varify ps))
   1.585       (fn (name, ps) => put_global_registration (name, map Logic.varify ps))