accomodate change of TheoryDataFun;
authorwenzelm
Fri Jun 17 18:35:27 2005 +0200 (2005-06-17)
changeset 164584c6fd0c01d28
parent 16457 e0f22edf38a5
child 16459 7efee005e568
accomodate change of TheoryDataFun;
accomodate identification of type Sign.sg and theory;
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/typedef_package.ML
src/Provers/Arith/fast_lin_arith.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/proof_context.ML
src/Pure/Proof/extraction.ML
src/Pure/axclass.ML
src/Pure/codegen.ML
src/Pure/goals.ML
src/Pure/meta_simplifier.ML
src/Pure/proofterm.ML
src/Pure/simplifier.ML
src/Sequents/prover.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/typechk.ML
     1.1 --- a/src/HOL/Tools/recdef_package.ML	Fri Jun 17 18:33:42 2005 +0200
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Fri Jun 17 18:35:27 2005 +0200
     1.3 @@ -103,28 +103,27 @@
     1.4  
     1.5  type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list};
     1.6  
     1.7 -structure GlobalRecdefArgs =
     1.8 -struct
     1.9 +structure GlobalRecdefData = TheoryDataFun
    1.10 +(struct
    1.11    val name = "HOL/recdef";
    1.12    type T = recdef_info Symtab.table * hints;
    1.13  
    1.14    val empty = (Symtab.empty, mk_hints ([], [], [])): T;
    1.15    val copy = I;
    1.16 -  val prep_ext = I;
    1.17 -  fun merge
    1.18 +  val extend = I;
    1.19 +  fun merge _
    1.20     ((tab1, {simps = simps1, congs = congs1, wfs = wfs1}),
    1.21 -    (tab2, {simps = simps2, congs = congs2, wfs = wfs2})) =
    1.22 +    (tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T =
    1.23        (Symtab.merge (K true) (tab1, tab2),
    1.24          mk_hints (Drule.merge_rules (simps1, simps2),
    1.25            Library.merge_alists congs1 congs2,
    1.26            Drule.merge_rules (wfs1, wfs2)));
    1.27  
    1.28 -  fun print sg (tab, hints) =
    1.29 -    (Pretty.strs ("recdefs:" :: map #1 (NameSpace.extern_table (Sign.const_space sg, tab))) ::
    1.30 +  fun print thy (tab, hints) =
    1.31 +    (Pretty.strs ("recdefs:" :: map #1 (NameSpace.extern_table (Sign.const_space thy, tab))) ::
    1.32        pretty_hints hints) |> Pretty.chunks |> Pretty.writeln;
    1.33 -end;
    1.34 +end);
    1.35  
    1.36 -structure GlobalRecdefData = TheoryDataFun(GlobalRecdefArgs);
    1.37  val print_recdefs = GlobalRecdefData.print;
    1.38  
    1.39  
    1.40 @@ -143,15 +142,14 @@
    1.41  
    1.42  (* proof data kind 'HOL/recdef' *)
    1.43  
    1.44 -structure LocalRecdefArgs =
    1.45 -struct
    1.46 +structure LocalRecdefData = ProofDataFun
    1.47 +(struct
    1.48    val name = "HOL/recdef";
    1.49    type T = hints;
    1.50    val init = get_global_hints;
    1.51    fun print _ hints = pretty_hints hints |> Pretty.chunks |> Pretty.writeln;
    1.52 -end;
    1.53 +end);
    1.54  
    1.55 -structure LocalRecdefData = ProofDataFun(LocalRecdefArgs);
    1.56  val get_local_hints = LocalRecdefData.get;
    1.57  val map_local_hints = LocalRecdefData.map;
    1.58  
    1.59 @@ -234,7 +232,7 @@
    1.60    let
    1.61      val _ = requires_recdef thy;
    1.62  
    1.63 -    val name = Sign.intern_const (Theory.sign_of thy) raw_name;
    1.64 +    val name = Sign.intern_const thy raw_name;
    1.65      val bname = Sign.base_name name;
    1.66      val _ = message ("Defining recursive function " ^ quote name ^ " ...");
    1.67  
    1.68 @@ -282,7 +280,7 @@
    1.69  
    1.70  fun gen_defer_recdef tfl_fn app_thms raw_name eqs raw_congs thy =
    1.71    let
    1.72 -    val name = Sign.intern_const (Theory.sign_of thy) raw_name;
    1.73 +    val name = Sign.intern_const thy raw_name;
    1.74      val bname = Sign.base_name name;
    1.75  
    1.76      val _ = requires_recdef thy;
    1.77 @@ -306,7 +304,7 @@
    1.78  
    1.79  fun gen_recdef_tc prep_att prep_name (bname, raw_atts) raw_name opt_i int thy =
    1.80    let
    1.81 -    val name = prep_name (Theory.sign_of thy) raw_name;
    1.82 +    val name = prep_name thy raw_name;
    1.83      val atts = map (prep_att thy) raw_atts;
    1.84      val tcs =
    1.85        (case get_recdef thy name of
    1.86 @@ -380,6 +378,4 @@
    1.87  
    1.88  end;
    1.89  
    1.90 -
    1.91  end;
    1.92 -
     2.1 --- a/src/HOL/Tools/record_package.ML	Fri Jun 17 18:33:42 2005 +0200
     2.2 +++ b/src/HOL/Tools/record_package.ML	Fri Jun 17 18:35:27 2005 +0200
     2.3 @@ -29,16 +29,16 @@
     2.4    val ext_typeN: string
     2.5    val last_extT: typ -> (string * typ list) option
     2.6    val dest_recTs : typ -> (string * typ list) list
     2.7 -  val get_extT_fields:  Sign.sg -> typ -> ((string * typ) list * (string * typ))
     2.8 -  val get_recT_fields:  Sign.sg -> typ -> ((string * typ) list * (string * typ))
     2.9 -  val get_extension: Sign.sg -> Symtab.key -> (string * typ list) option
    2.10 -  val get_extinjects: Sign.sg -> thm list
    2.11 -  val get_simpset: Sign.sg -> simpset
    2.12 +  val get_extT_fields:  theory -> typ -> ((string * typ) list * (string * typ))
    2.13 +  val get_recT_fields:  theory -> typ -> ((string * typ) list * (string * typ))
    2.14 +  val get_extension: theory -> Symtab.key -> (string * typ list) option
    2.15 +  val get_extinjects: theory -> thm list
    2.16 +  val get_simpset: theory -> simpset
    2.17    val print_records: theory -> unit
    2.18 -  val add_record: string list * string -> string option -> (string * string * mixfix) list 
    2.19 -                  -> theory -> theory
    2.20 -  val add_record_i: string list * string -> (typ list * string) option 
    2.21 -                    -> (string * typ * mixfix) list -> theory -> theory
    2.22 +  val add_record: string list * string -> string option -> (string * string * mixfix) list
    2.23 +    -> theory -> theory
    2.24 +  val add_record_i: string list * string -> (typ list * string) option
    2.25 +    -> (string * typ * mixfix) list -> theory -> theory
    2.26    val setup: (theory -> theory) list
    2.27  end;
    2.28  
    2.29 @@ -235,8 +235,8 @@
    2.30    equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits, 
    2.31    extfields = extfields, fieldext = fieldext }: record_data;
    2.32  
    2.33 -structure RecordsArgs =
    2.34 -struct
    2.35 +structure RecordsData = TheoryDataFun
    2.36 +(struct
    2.37    val name = "HOL/records";       
    2.38    type T = record_data;
    2.39  
    2.40 @@ -246,8 +246,8 @@
    2.41         Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
    2.42  
    2.43    val copy = I;
    2.44 -  val prep_ext = I;
    2.45 -  fun merge
    2.46 +  val extend = I;
    2.47 +  fun merge _
    2.48     ({records = recs1,
    2.49       sel_upd = {selectors = sels1, updates = upds1, simpset = ss1},
    2.50       equalities = equalities1,
    2.51 @@ -296,11 +296,11 @@
    2.52            [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
    2.53            pretty_parent parent @ map pretty_field fields));
    2.54      in map pretty_record (Symtab.dest recs) |> Pretty.chunks |> Pretty.writeln end;
    2.55 -end;
    2.56 +end);
    2.57  
    2.58 -structure RecordsData = TheoryDataFun(RecordsArgs);
    2.59  val print_records = RecordsData.print;
    2.60  
    2.61 +
    2.62  (* access 'records' *)
    2.63  
    2.64  fun get_record thy name = Symtab.lookup (#records (RecordsData.get thy), name);
    2.65 @@ -315,7 +315,7 @@
    2.66  
    2.67  (* access 'sel_upd' *)
    2.68  
    2.69 -fun get_sel_upd sg = #sel_upd (RecordsData.get_sg sg);
    2.70 +val get_sel_upd = #sel_upd o RecordsData.get;
    2.71  
    2.72  fun get_selectors sg name = Symtab.lookup (#selectors (get_sel_upd sg), name);
    2.73  fun is_selector sg name = 
    2.74 @@ -353,7 +353,7 @@
    2.75    in RecordsData.put data thy end;
    2.76  
    2.77  fun get_equalities sg name =
    2.78 -  Symtab.lookup (#equalities (RecordsData.get_sg sg), name);
    2.79 +  Symtab.lookup (#equalities (RecordsData.get sg), name);
    2.80  
    2.81  (* access 'extinjects' *)
    2.82  
    2.83 @@ -365,7 +365,7 @@
    2.84                   splits extfields fieldext;
    2.85    in RecordsData.put data thy end;
    2.86  
    2.87 -fun get_extinjects sg = #extinjects (RecordsData.get_sg sg);
    2.88 +fun get_extinjects sg = #extinjects (RecordsData.get sg);
    2.89  
    2.90  (* access 'extsplit' *)
    2.91  
    2.92 @@ -379,7 +379,7 @@
    2.93    in RecordsData.put data thy end;
    2.94  
    2.95  fun get_extsplit sg name =
    2.96 -  Symtab.lookup (#extsplit (RecordsData.get_sg sg), name);
    2.97 +  Symtab.lookup (#extsplit (RecordsData.get sg), name);
    2.98  
    2.99  (* access 'splits' *)
   2.100  
   2.101 @@ -393,13 +393,13 @@
   2.102    in RecordsData.put data thy end;
   2.103  
   2.104  fun get_splits sg name =
   2.105 -  Symtab.lookup (#splits (RecordsData.get_sg sg), name);
   2.106 +  Symtab.lookup (#splits (RecordsData.get sg), name);
   2.107  
   2.108  
   2.109  
   2.110  (* extension of a record name *)
   2.111  fun get_extension sg name =
   2.112 - case Symtab.lookup (#records (RecordsData.get_sg sg),name) of
   2.113 + case Symtab.lookup (#records (RecordsData.get sg),name) of
   2.114          SOME s => SOME (#extension s)
   2.115        | NONE => NONE;
   2.116  
   2.117 @@ -415,7 +415,7 @@
   2.118    in RecordsData.put data thy end;
   2.119  
   2.120  fun get_extfields sg name =
   2.121 -  Symtab.lookup (#extfields (RecordsData.get_sg sg), name);
   2.122 +  Symtab.lookup (#extfields (RecordsData.get sg), name);
   2.123  
   2.124  fun get_extT_fields sg T = 
   2.125    let
   2.126 @@ -425,7 +425,7 @@
   2.127      val midx = maxidx_of_typs (moreT::Ts);
   2.128      fun varify (a, S) = TVar ((a, midx), S);
   2.129      val varifyT = map_type_tfree varify;
   2.130 -    val {records,extfields,...} = RecordsData.get_sg sg;
   2.131 +    val {records,extfields,...} = RecordsData.get sg;
   2.132      val (flds,(more,_)) = split_last (Symtab.lookup_multi (extfields,name));
   2.133      val args = map varifyT (snd (#extension (valOf (Symtab.lookup (records,recname)))));
   2.134  
   2.135 @@ -458,7 +458,7 @@
   2.136  
   2.137  
   2.138  fun get_fieldext sg name =
   2.139 -  Symtab.lookup (#fieldext (RecordsData.get_sg sg), name);
   2.140 +  Symtab.lookup (#fieldext (RecordsData.get sg), name);
   2.141  
   2.142  (* parent records *)
   2.143  
   2.144 @@ -841,7 +841,7 @@
   2.145  
   2.146  fun prove_split_simp sg T prop =
   2.147    let 
   2.148 -    val {sel_upd={simpset,...},extsplit,...} = RecordsData.get_sg sg;
   2.149 +    val {sel_upd={simpset,...},extsplit,...} = RecordsData.get sg;
   2.150      val extsplits = 
   2.151              Library.foldl (fn (thms,(n,_)) => (list (Symtab.lookup (extsplit,n)))@thms) 
   2.152                      ([],dest_recTs T);
   2.153 @@ -880,7 +880,7 @@
   2.154            (case get_updates sg u of SOME u_name =>
   2.155              let
   2.156                fun mk_abs_var x t = (x, fastype_of t);
   2.157 -              val {sel_upd={updates,...},extfields,...} = RecordsData.get_sg sg;
   2.158 +              val {sel_upd={updates,...},extfields,...} = RecordsData.get sg;
   2.159                
   2.160                fun mk_eq_terms ((upd as Const (u,Type(_,[updT,_]))) $ k $ r) =
   2.161  		  (case (Symtab.lookup (updates,u)) of
   2.162 @@ -938,7 +938,7 @@
   2.163      (fn sg => fn _ => fn t =>
   2.164        (case t of ((upd as Const (u, Type(_,[_,Type(_,[T,_])]))) $ k $ r) =>
   2.165   	 let datatype ('a,'b) calc = Init of 'b | Inter of 'a  
   2.166 -             val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get_sg sg;
   2.167 +             val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get sg;
   2.168               
   2.169  	     fun mk_abs_var x t = (x, fastype_of t);
   2.170               fun sel_name u = NameSpace.base (unsuffix updateN u);
   2.171 @@ -1142,7 +1142,7 @@
   2.172    let
   2.173      val sg = Thm.sign_of_thm st;
   2.174      val {sel_upd={simpset,...},...} 
   2.175 -            = RecordsData.get_sg sg;
   2.176 +            = RecordsData.get sg;
   2.177  
   2.178      val has_rec = exists_Const
   2.179        (fn (s, Type (_, [Type (_, [T, _]), _])) =>
     3.1 --- a/src/HOL/Tools/typedef_package.ML	Fri Jun 17 18:33:42 2005 +0200
     3.2 +++ b/src/HOL/Tools/typedef_package.ML	Fri Jun 17 18:35:27 2005 +0200
     3.3 @@ -1,6 +1,6 @@
     3.4  (*  Title:      HOL/Tools/typedef_package.ML
     3.5      ID:         $Id$
     3.6 -    Author:     Markus Wenzel, TU Muenchen
     3.7 +    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
     3.8  
     3.9  Gordon/HOL-style type definitions.
    3.10  *)
    3.11 @@ -50,18 +50,16 @@
    3.12  
    3.13  (** theory data **)
    3.14  
    3.15 -structure TypedefArgs =
    3.16 -struct
    3.17 +structure TypedefData = TheoryDataFun
    3.18 +(struct
    3.19    val name = "HOL/typedef";
    3.20    type T = (typ * typ * string * string) Symtab.table;
    3.21    val empty = Symtab.empty;
    3.22    val copy = I;
    3.23 -  val prep_ext = I;
    3.24 -  val merge : T * T -> T = Symtab.merge op =;
    3.25 -  fun print sg _ = ();
    3.26 -end;
    3.27 -
    3.28 -structure TypedefData = TheoryDataFun(TypedefArgs);
    3.29 +  val extend = I;
    3.30 +  fun merge _ (tabs: T * T) = Symtab.merge (op =) tabs;
    3.31 +  fun print _ _ = ();
    3.32 +end);
    3.33  
    3.34  fun put_typedef newT oldT Abs_name Rep_name thy =
    3.35    TypedefData.put (Symtab.update_new
    3.36 @@ -74,16 +72,14 @@
    3.37  
    3.38  fun add_typedecls decls thy =
    3.39    let
    3.40 -    val full = Sign.full_name (Theory.sign_of thy);
    3.41 -
    3.42      fun arity_of (raw_name, args, mx) =
    3.43 -      (full (Syntax.type_name raw_name mx), replicate (length args) HOLogic.typeS, HOLogic.typeS);
    3.44 +      (Sign.full_name thy (Syntax.type_name raw_name mx),
    3.45 +        replicate (length args) HOLogic.typeS, HOLogic.typeS);
    3.46    in
    3.47      if can (Theory.assert_super HOL.thy) thy then
    3.48 -      thy
    3.49 -      |> PureThy.add_typedecls decls
    3.50 +      thy |> Theory.add_typedecls decls
    3.51        |> Theory.add_arities_i (map arity_of decls)
    3.52 -    else thy |> PureThy.add_typedecls decls
    3.53 +    else thy |> Theory.add_typedecls decls
    3.54    end;
    3.55  
    3.56  
    3.57 @@ -109,16 +105,17 @@
    3.58        getOpt (witn2_tac, TRY (ALLGOALS (CLASET' blast_tac)));
    3.59    in
    3.60      message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ...");
    3.61 -    Tactic.prove (Theory.sign_of thy) [] [] goal (K tac)
    3.62 -  end handle ERROR => error ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset));
    3.63 +    Tactic.prove thy [] [] goal (K tac)
    3.64 +  end
    3.65 +  handle ERROR => error ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset));
    3.66  
    3.67  
    3.68  (* prepare_typedef *)
    3.69  
    3.70 -fun read_term sg used s =
    3.71 -  #1 (Thm.read_def_cterm (sg, K NONE, K NONE) used true (s, HOLogic.typeT));
    3.72 +fun read_term thy used s =
    3.73 +  #1 (Thm.read_def_cterm (thy, K NONE, K NONE) used true (s, HOLogic.typeT));
    3.74  
    3.75 -fun cert_term sg _ t = Thm.cterm_of sg t handle TERM (msg, _) => error msg;
    3.76 +fun cert_term thy _ t = Thm.cterm_of thy t handle TERM (msg, _) => error msg;
    3.77  
    3.78  fun err_in_typedef name =
    3.79    error ("The error(s) above occurred in typedef " ^ quote name);
    3.80 @@ -126,16 +123,15 @@
    3.81  fun prepare_typedef prep_term def name (t, vs, mx) raw_set opt_morphs thy =
    3.82    let
    3.83      val _ = Theory.requires thy "Typedef" "typedefs";
    3.84 -    val sign = Theory.sign_of thy;
    3.85 -    val full = Sign.full_name sign;
    3.86 +    val full = Sign.full_name thy;
    3.87  
    3.88      (*rhs*)
    3.89      val full_name = full name;
    3.90 -    val cset = prep_term sign vs raw_set;
    3.91 +    val cset = prep_term thy vs raw_set;
    3.92      val {T = setT, t = set, ...} = Thm.rep_cterm cset;
    3.93      val rhs_tfrees = term_tfrees set;
    3.94      val oldT = HOLogic.dest_setT setT handle TYPE _ =>
    3.95 -      error ("Not a set type: " ^ quote (Sign.string_of_typ sign setT));
    3.96 +      error ("Not a set type: " ^ quote (Sign.string_of_typ thy setT));
    3.97      fun mk_nonempty A =
    3.98        HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)));
    3.99      val goal = mk_nonempty set;
   3.100 @@ -283,7 +279,7 @@
   3.101          val (gr', _) = Codegen.invoke_tycodegen thy dep false (gr, T);
   3.102          val (gr'', ps) =
   3.103            foldl_map (Codegen.invoke_codegen thy dep true) (gr', ts);
   3.104 -        val id = Codegen.mk_const_id (sign_of thy) s
   3.105 +        val id = Codegen.mk_const_id thy s
   3.106        in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end;
   3.107      fun get_name (Type (tname, _)) = tname
   3.108        | get_name _ = "";
   3.109 @@ -312,10 +308,9 @@
   3.110         | SOME (newT as Type (tname, Us), oldT, Abs_name, Rep_name) =>
   3.111             if isSome (Codegen.get_assoc_type thy tname) then NONE else
   3.112             let
   3.113 -             val sg = sign_of thy;
   3.114 -             val Abs_id = Codegen.mk_const_id sg Abs_name;
   3.115 -             val Rep_id = Codegen.mk_const_id sg Rep_name;
   3.116 -             val ty_id = Codegen.mk_type_id sg s;
   3.117 +             val Abs_id = Codegen.mk_const_id thy Abs_name;
   3.118 +             val Rep_id = Codegen.mk_const_id thy Rep_name;
   3.119 +             val ty_id = Codegen.mk_type_id thy s;
   3.120               val (gr', qs) = foldl_map
   3.121                 (Codegen.invoke_tycodegen thy dep (length Ts = 1)) (gr, Ts);
   3.122               val gr'' = Graph.add_edge (Abs_id, dep) gr' handle Graph.UNDEF _ =>
   3.123 @@ -334,21 +329,21 @@
   3.124                       Pretty.str "x) = x;"]) ^ "\n\n" ^
   3.125                     (if "term_of" mem !Codegen.mode then
   3.126                        Pretty.string_of (Pretty.block [Pretty.str "fun ",
   3.127 -                        Codegen.mk_term_of sg false newT, Pretty.brk 1,
   3.128 +                        Codegen.mk_term_of thy false newT, Pretty.brk 1,
   3.129                          Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
   3.130                          Pretty.str "x) =", Pretty.brk 1,
   3.131                          Pretty.block [Pretty.str ("Const (\"" ^ Abs_name ^ "\","),
   3.132                            Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
   3.133                            Pretty.str ")"], Pretty.str " $", Pretty.brk 1,
   3.134 -                        Codegen.mk_term_of sg false oldT, Pretty.brk 1,
   3.135 +                        Codegen.mk_term_of thy false oldT, Pretty.brk 1,
   3.136                          Pretty.str "x;"]) ^ "\n\n"
   3.137                      else "") ^
   3.138                     (if "test" mem !Codegen.mode then
   3.139                        Pretty.string_of (Pretty.block [Pretty.str "fun ",
   3.140 -                        Codegen.mk_gen sg false [] "" newT, Pretty.brk 1,
   3.141 +                        Codegen.mk_gen thy false [] "" newT, Pretty.brk 1,
   3.142                          Pretty.str "i =", Pretty.brk 1,
   3.143                          Pretty.block [Pretty.str (Abs_id ^ " ("),
   3.144 -                          Codegen.mk_gen sg false [] "" oldT, Pretty.brk 1,
   3.145 +                          Codegen.mk_gen thy false [] "" oldT, Pretty.brk 1,
   3.146                            Pretty.str "i);"]]) ^ "\n\n"
   3.147                      else "")
   3.148                 in Graph.map_node Abs_id (K (NONE, s)) gr'' end
     4.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Fri Jun 17 18:33:42 2005 +0200
     4.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Fri Jun 17 18:35:27 2005 +0200
     4.3 @@ -11,7 +11,7 @@
     4.4  
     4.5  and a simplification procedure
     4.6  
     4.7 -    lin_arith_prover: Sign.sg -> simpset -> term -> thm option
     4.8 +    lin_arith_prover: theory -> simpset -> term -> thm option
     4.9  
    4.10  Only take premises and conclusions into account that are already (negated)
    4.11  (in)equations. lin_arith_prover tries to prove or disprove the term.
    4.12 @@ -34,7 +34,7 @@
    4.13    val neg_prop: term -> term
    4.14    val is_False: thm -> bool
    4.15    val is_nat: typ list * term -> bool
    4.16 -  val mk_nat_thm: Sign.sg -> term -> thm
    4.17 +  val mk_nat_thm: theory -> term -> thm
    4.18  end;
    4.19  (*
    4.20  mk_Eq(~in) = `in == False'
    4.21 @@ -52,7 +52,7 @@
    4.22  signature LIN_ARITH_DATA =
    4.23  sig
    4.24    val decomp:
    4.25 -    Sign.sg -> term -> ((term*rat)list * rat * string * (term*rat)list * rat * bool)option
    4.26 +    theory -> term -> ((term*rat)list * rat * string * (term*rat)list * rat * bool)option
    4.27    val number_of: IntInf.int * typ -> term
    4.28  end;
    4.29  (*
    4.30 @@ -77,7 +77,7 @@
    4.31                  -> theory -> theory
    4.32    val trace           : bool ref
    4.33    val fast_arith_neq_limit: int ref
    4.34 -  val lin_arith_prover: Sign.sg -> simpset -> term -> thm option
    4.35 +  val lin_arith_prover: theory -> simpset -> term -> thm option
    4.36    val     lin_arith_tac:     bool -> int -> tactic
    4.37    val cut_lin_arith_tac: thm list -> int -> tactic
    4.38  end;
    4.39 @@ -91,8 +91,8 @@
    4.40  
    4.41  (* data kind 'Provers/fast_lin_arith' *)
    4.42  
    4.43 -structure DataArgs =
    4.44 -struct
    4.45 +structure Data = TheoryDataFun
    4.46 +(struct
    4.47    val name = "Provers/fast_lin_arith";
    4.48    type T = {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
    4.49              lessD: thm list, neqE: thm list, simpset: Simplifier.simpset};
    4.50 @@ -100,12 +100,13 @@
    4.51    val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [],
    4.52                 lessD = [], neqE = [], simpset = Simplifier.empty_ss};
    4.53    val copy = I;
    4.54 -  val prep_ext = I;
    4.55 +  val extend = I;
    4.56  
    4.57 -  fun merge ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1,
    4.58 -              lessD = lessD1, neqE=neqE1, simpset = simpset1},
    4.59 -             {add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2,
    4.60 -              lessD = lessD2, neqE=neqE2, simpset = simpset2}) =
    4.61 +  fun merge _
    4.62 +    ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1,
    4.63 +      lessD = lessD1, neqE=neqE1, simpset = simpset1},
    4.64 +     {add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2,
    4.65 +      lessD = lessD2, neqE=neqE2, simpset = simpset2}) =
    4.66      {add_mono_thms = Drule.merge_rules (add_mono_thms1, add_mono_thms2),
    4.67       mult_mono_thms = Drule.merge_rules (mult_mono_thms1, mult_mono_thms2),
    4.68       inj_thms = Drule.merge_rules (inj_thms1, inj_thms2),
    4.69 @@ -114,9 +115,8 @@
    4.70       simpset = Simplifier.merge_ss (simpset1, simpset2)};
    4.71  
    4.72    fun print _ _ = ();
    4.73 -end;
    4.74 +end);
    4.75  
    4.76 -structure Data = TheoryDataFun(DataArgs);
    4.77  val map_data = Data.map;
    4.78  val setup = [Data.init];
    4.79  
    4.80 @@ -420,7 +420,7 @@
    4.81  in
    4.82  fun mkthm sg asms just =
    4.83    let val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} =
    4.84 -          Data.get_sg sg;
    4.85 +          Data.get sg;
    4.86        val atoms = Library.foldl (fn (ats,(lhs,_,_,rhs,_,_)) =>
    4.87                              map fst lhs  union  (map fst rhs  union  ats))
    4.88                          ([], List.mapPartial (fn thm => if Thm.no_prems thm
    4.89 @@ -625,7 +625,7 @@
    4.90  fun refute_tac(i,justs) =
    4.91    fn state =>
    4.92      let val sg = #sign(rep_thm state)
    4.93 -        val {neqE, ...} = Data.get_sg sg;
    4.94 +        val {neqE, ...} = Data.get sg;
    4.95          fun just1 j = REPEAT_DETERM(eresolve_tac neqE i) THEN
    4.96                        METAHYPS (fn asms => rtac (mkthm sg asms j) 1) i
    4.97      in DETERM(resolve_tac [LA_Logic.notI,LA_Logic.ccontr] i) THEN
    4.98 @@ -691,7 +691,7 @@
    4.99  in (ct1,ct2) end;
   4.100  
   4.101  fun splitasms sg asms =
   4.102 -let val {neqE, ...}  = Data.get_sg sg;
   4.103 +let val {neqE, ...}  = Data.get sg;
   4.104      fun split(asms',[]) = Tip(rev asms')
   4.105        | split(asms',asm::asms) =
   4.106        (case get_first (fn th => SOME(asm COMP th) handle THM _ => NONE) neqE
     5.1 --- a/src/Pure/Isar/attrib.ML	Fri Jun 17 18:33:42 2005 +0200
     5.2 +++ b/src/Pure/Isar/attrib.ML	Fri Jun 17 18:35:27 2005 +0200
     5.3 @@ -8,8 +8,9 @@
     5.4  signature BASIC_ATTRIB =
     5.5  sig
     5.6    val print_attributes: theory -> unit
     5.7 -  val Attribute: bstring -> (Args.src -> theory attribute) * (Args.src -> ProofContext.context attribute)
     5.8 -    -> string -> unit
     5.9 +  val Attribute: bstring ->
    5.10 +    (Args.src -> theory attribute) * (Args.src -> ProofContext.context attribute) ->
    5.11 +    string -> unit
    5.12  end;
    5.13  
    5.14  signature ATTRIB =
    5.15 @@ -17,8 +18,8 @@
    5.16    include BASIC_ATTRIB
    5.17    type src
    5.18    exception ATTRIB_FAIL of (string * Position.T) * exn
    5.19 -  val intern: Sign.sg -> xstring -> string
    5.20 -  val intern_src: Sign.sg -> src -> src
    5.21 +  val intern: theory -> xstring -> string
    5.22 +  val intern_src: theory -> src -> src
    5.23    val global_attribute_i: theory -> src -> theory attribute
    5.24    val global_attribute: theory -> src -> theory attribute
    5.25    val local_attribute_i: theory -> src -> ProofContext.context attribute
    5.26 @@ -33,9 +34,12 @@
    5.27    val global_thm: theory * Args.T list -> thm * (theory * Args.T list)
    5.28    val global_thms: theory * Args.T list -> thm list * (theory * Args.T list)
    5.29    val global_thmss: theory * Args.T list -> thm list * (theory * Args.T list)
    5.30 -  val local_thm: ProofContext.context * Args.T list -> thm * (ProofContext.context * Args.T list)
    5.31 -  val local_thms: ProofContext.context * Args.T list -> thm list * (ProofContext.context * Args.T list)
    5.32 -  val local_thmss: ProofContext.context * Args.T list -> thm list * (ProofContext.context * Args.T list)
    5.33 +  val local_thm: ProofContext.context * Args.T list ->
    5.34 +    thm * (ProofContext.context * Args.T list)
    5.35 +  val local_thms: ProofContext.context * Args.T list ->
    5.36 +    thm list * (ProofContext.context * Args.T list)
    5.37 +  val local_thmss: ProofContext.context * Args.T list ->
    5.38 +    thm list * (ProofContext.context * Args.T list)
    5.39    val syntax: ('a * Args.T list -> 'a attribute * ('a * Args.T list)) -> src -> 'a attribute
    5.40    val no_args: 'a attribute -> src -> 'a attribute
    5.41    val add_del_args: 'a attribute -> 'a attribute -> src -> 'a attribute
    5.42 @@ -50,10 +54,10 @@
    5.43  
    5.44  (** attributes theory data **)
    5.45  
    5.46 -(* data kind 'Isar/attributes' *)
    5.47 +(* datatype attributes *)
    5.48  
    5.49 -structure AttributesDataArgs =
    5.50 -struct
    5.51 +structure AttributesData = TheoryDataFun
    5.52 +(struct
    5.53    val name = "Isar/attributes";
    5.54    type T =
    5.55      ((((src -> theory attribute) * (src -> ProofContext.context attribute))
    5.56 @@ -61,9 +65,9 @@
    5.57  
    5.58    val empty = NameSpace.empty_table;
    5.59    val copy = I;
    5.60 -  val prep_ext = I;
    5.61 +  val extend = I;
    5.62  
    5.63 -  fun merge tables = NameSpace.merge_tables eq_snd tables handle Symtab.DUPS dups =>
    5.64 +  fun merge _ tables = NameSpace.merge_tables eq_snd tables handle Symtab.DUPS dups =>
    5.65      error ("Attempt to merge different versions of attribute(s) " ^ commas_quote dups);
    5.66  
    5.67    fun print _ attribs =
    5.68 @@ -74,16 +78,15 @@
    5.69        [Pretty.big_list "attributes:" (map prt_attr (NameSpace.extern_table attribs))]
    5.70        |> Pretty.chunks |> Pretty.writeln
    5.71      end;
    5.72 -end;
    5.73 +end);
    5.74  
    5.75 -structure AttributesData = TheoryDataFun(AttributesDataArgs);
    5.76  val _ = Context.add_setup [AttributesData.init];
    5.77  val print_attributes = AttributesData.print;
    5.78  
    5.79  
    5.80  (* interning *)
    5.81  
    5.82 -val intern = NameSpace.intern o #1 o AttributesData.get_sg;
    5.83 +val intern = NameSpace.intern o #1 o AttributesData.get;
    5.84  val intern_src = Args.map_name o intern;
    5.85  
    5.86  
    5.87 @@ -103,10 +106,10 @@
    5.88    in attr end;
    5.89  
    5.90  val global_attribute_i = gen_attribute fst;
    5.91 -fun global_attribute thy = global_attribute_i thy o intern_src (Theory.sign_of thy);
    5.92 +fun global_attribute thy = global_attribute_i thy o intern_src thy;
    5.93  
    5.94  val local_attribute_i = gen_attribute snd;
    5.95 -fun local_attribute thy = local_attribute_i thy o intern_src (Theory.sign_of thy);
    5.96 +fun local_attribute thy = local_attribute_i thy o intern_src thy;
    5.97  
    5.98  val context_attribute_i = local_attribute_i o ProofContext.theory_of;
    5.99  val context_attribute = local_attribute o ProofContext.theory_of;
   5.100 @@ -133,10 +136,9 @@
   5.101  
   5.102  fun add_attributes raw_attrs thy =
   5.103    let
   5.104 -    val sg = Theory.sign_of thy;
   5.105      val new_attrs = raw_attrs |> map (fn (name, (f, g), comment) =>
   5.106        (name, (((f, g), comment), stamp ())));
   5.107 -    fun add attrs = NameSpace.extend_table (Sign.naming_of sg) (attrs, new_attrs)
   5.108 +    fun add attrs = NameSpace.extend_table (Sign.naming_of thy) (attrs, new_attrs)
   5.109        handle Symtab.DUPS dups =>
   5.110          error ("Duplicate declaration of attributes(s) " ^ commas_quote dups);
   5.111    in AttributesData.map add thy end;
   5.112 @@ -157,7 +159,7 @@
   5.113  
   5.114  fun gen_thm theory_of attrib get pick = Scan.depend (fn st =>
   5.115    Scan.ahead Args.name -- Args.named_fact (fn name => get st (name, NONE)) --
   5.116 -  Scan.option Args.thm_sel -- Args.opt_attribs (intern (Theory.sign_of (theory_of st)))
   5.117 +  Scan.option Args.thm_sel -- Args.opt_attribs (intern (theory_of st))
   5.118    >> (fn (((name, fact), sel), srcs) =>
   5.119      let
   5.120        val ths = PureThy.select_thm (name, sel) fact;
   5.121 @@ -238,24 +240,24 @@
   5.122  fun the_type types xi = the (types xi)
   5.123    handle Option.Option => error_var "No such variable in theorem: " xi;
   5.124  
   5.125 -fun unify_types sign types ((unifier, maxidx), (xi, u)) =
   5.126 +fun unify_types thy types ((unifier, maxidx), (xi, u)) =
   5.127    let
   5.128      val T = the_type types xi;
   5.129      val U = Term.fastype_of u;
   5.130      val maxidx' = Int.max (maxidx, Int.max (#2 xi, Term.maxidx_of_term u));
   5.131    in
   5.132 -    Type.unify (Sign.tsig_of sign) (unifier, maxidx') (T, U)
   5.133 +    Type.unify (Sign.tsig_of thy) (unifier, maxidx') (T, U)
   5.134        handle Type.TUNIFY => error_var "Incompatible type for instantiation of " xi
   5.135    end;
   5.136  
   5.137  fun typ_subst env = apsnd (Term.typ_subst_TVars env);
   5.138  fun subst env = apsnd (Term.subst_TVars env);
   5.139  
   5.140 -fun instantiate sign envT env thm =
   5.141 +fun instantiate thy envT env thm =
   5.142    let
   5.143      val (_, sorts) = Drule.types_sorts thm;
   5.144 -    fun prepT (a, T) = (Thm.ctyp_of sign (TVar (a, the_sort sorts a)), Thm.ctyp_of sign T);
   5.145 -    fun prep (xi, t) = pairself (Thm.cterm_of sign) (Var (xi, Term.fastype_of t), t);
   5.146 +    fun prepT (a, T) = (Thm.ctyp_of thy (TVar (a, the_sort sorts a)), Thm.ctyp_of thy T);
   5.147 +    fun prep (xi, t) = pairself (Thm.cterm_of thy) (Var (xi, Term.fastype_of t), t);
   5.148    in
   5.149      Drule.instantiate (map prepT (distinct envT),
   5.150        map prep (gen_distinct (fn ((xi, t), (yj, u)) => xi = yj andalso t aconv u) env)) thm
   5.151 @@ -266,7 +268,7 @@
   5.152  fun read_instantiate init mixed_insts (context, thm) =
   5.153    let
   5.154      val ctxt = init context;
   5.155 -    val sign = ProofContext.sign_of ctxt;
   5.156 +    val thy = ProofContext.theory_of ctxt;
   5.157  
   5.158      val (type_insts, term_insts) = List.partition (is_tvar o #1) (map #2 mixed_insts);
   5.159      val internal_insts = term_insts |> List.mapPartial
   5.160 @@ -290,23 +292,23 @@
   5.161            | Args.Typ T => T
   5.162            | _ => error_var "Type argument expected for " xi);
   5.163        in
   5.164 -        if Sign.of_sort sign (T, S) then (xi, T)
   5.165 +        if Sign.of_sort thy (T, S) then (xi, T)
   5.166          else error_var "Incompatible sort for typ instantiation of " xi
   5.167        end;
   5.168  
   5.169      val type_insts' = map readT type_insts;
   5.170 -    val thm' = instantiate sign type_insts' [] thm;
   5.171 +    val thm' = instantiate thy type_insts' [] thm;
   5.172  
   5.173  
   5.174      (* internal term instantiations *)
   5.175  
   5.176      val types' = #1 (Drule.types_sorts thm');
   5.177      val unifier = map (apsnd snd) (Vartab.dest (#1
   5.178 -      (Library.foldl (unify_types sign types') ((Vartab.empty, 0), internal_insts))));
   5.179 +      (Library.foldl (unify_types thy types') ((Vartab.empty, 0), internal_insts))));
   5.180  
   5.181      val type_insts'' = map (typ_subst unifier) type_insts';
   5.182      val internal_insts'' = map (subst unifier) internal_insts;
   5.183 -    val thm'' = instantiate sign unifier internal_insts'' thm';
   5.184 +    val thm'' = instantiate thy unifier internal_insts'' thm';
   5.185  
   5.186  
   5.187      (* external term instantiations *)
   5.188 @@ -323,7 +325,7 @@
   5.189  
   5.190      val external_insts''' = xs ~~ ts;
   5.191      val term_insts''' = internal_insts''' @ external_insts''';
   5.192 -    val thm''' = instantiate sign inferred external_insts''' thm'';
   5.193 +    val thm''' = instantiate thy inferred external_insts''' thm'';
   5.194    in
   5.195  
   5.196      (* assign internalized values *)
     6.1 --- a/src/Pure/Isar/locale.ML	Fri Jun 17 18:33:42 2005 +0200
     6.2 +++ b/src/Pure/Isar/locale.ML	Fri Jun 17 18:35:27 2005 +0200
     6.3 @@ -44,8 +44,8 @@
     6.4    type element
     6.5    type element_i
     6.6    type locale
     6.7 -  val intern: Sign.sg -> xstring -> string
     6.8 -  val extern: Sign.sg -> string -> xstring
     6.9 +  val intern: theory -> xstring -> string
    6.10 +  val extern: theory -> string -> xstring
    6.11    val the_locale: theory -> string -> locale
    6.12    val intern_attrib_elem: theory ->
    6.13      ('typ, 'term, 'fact) elem -> ('typ, 'term, 'fact) elem
    6.14 @@ -161,11 +161,11 @@
    6.15        then t
    6.16        else Term.map_term_types (tinst_tab_type tinst) t;
    6.17  
    6.18 -fun tinst_tab_thm sg tinst thm = if Symtab.is_empty tinst
    6.19 +fun tinst_tab_thm thy tinst thm = if Symtab.is_empty tinst
    6.20        then thm
    6.21        else let
    6.22 -          val cert = Thm.cterm_of sg;
    6.23 -          val certT = Thm.ctyp_of sg;
    6.24 +          val cert = Thm.cterm_of thy;
    6.25 +          val certT = Thm.ctyp_of thy;
    6.26            val {hyps, prop, ...} = Thm.rep_thm thm;
    6.27            val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
    6.28            val tinst' = Symtab.dest tinst |>
    6.29 @@ -198,11 +198,11 @@
    6.30              | instf (s $ t) = instf s $ instf t
    6.31          in instf end;
    6.32  
    6.33 -fun inst_tab_thm sg (inst, tinst) thm = if Symtab.is_empty inst
    6.34 -      then tinst_tab_thm sg tinst thm
    6.35 +fun inst_tab_thm thy (inst, tinst) thm = if Symtab.is_empty inst
    6.36 +      then tinst_tab_thm thy tinst thm
    6.37        else let
    6.38 -          val cert = Thm.cterm_of sg;
    6.39 -          val certT = Thm.ctyp_of sg;
    6.40 +          val cert = Thm.cterm_of thy;
    6.41 +          val certT = Thm.ctyp_of thy;
    6.42            val {hyps, prop, ...} = Thm.rep_thm thm;
    6.43            (* type instantiations *)
    6.44            val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
    6.45 @@ -218,7 +218,7 @@
    6.46                      if a = x then SOME (Free (x, tinst_tab_type tinst T), t)
    6.47                      else NONE) frees);
    6.48          in
    6.49 -          if null tinst' andalso null inst' then tinst_tab_thm sg tinst thm
    6.50 +          if null tinst' andalso null inst' then tinst_tab_thm thy tinst thm
    6.51            else thm |> Drule.implies_intr_list (map cert hyps)
    6.52              |> Drule.tvars_intr_list (map #1 tinst')
    6.53              |> (fn (th, al) => th |> Thm.instantiate
    6.54 @@ -239,9 +239,9 @@
    6.55      val empty: T
    6.56      val join: T * T -> T
    6.57      val dest: T -> (term list * ((string * Attrib.src list) * thm list)) list
    6.58 -    val lookup: Sign.sg -> T * term list ->
    6.59 +    val lookup: theory -> T * term list ->
    6.60        ((string * Attrib.src list) * thm list) option
    6.61 -    val insert: Sign.sg -> term list * (string * Attrib.src list) -> T ->
    6.62 +    val insert: theory -> term list * (string * Attrib.src list) -> T ->
    6.63        T * (term list * ((string * Attrib.src list) * thm list)) list
    6.64      val add_witness: term list -> thm -> T -> T
    6.65    end =
    6.66 @@ -262,7 +262,7 @@
    6.67  
    6.68    (* joining of registrations: prefix and attributs of left theory,
    6.69       thms are equal, no attempt to subsumption testing *)
    6.70 -  fun join (r1, r2) = Termtab.join (fn (reg, _) => SOME reg) (r1, r2);
    6.71 +  fun join (r1, r2) = Termtab.join (fn _ => fn (reg, _) => SOME reg) (r1, r2);
    6.72  
    6.73    fun dest regs = map (apfst untermify) (Termtab.dest regs);
    6.74  
    6.75 @@ -321,8 +321,8 @@
    6.76  
    6.77  (** theory data **)
    6.78  
    6.79 -structure GlobalLocalesArgs =
    6.80 -struct
    6.81 +structure GlobalLocalesData = TheoryDataFun
    6.82 +(struct
    6.83    val name = "Isar/locales";
    6.84    type T = NameSpace.T * locale Symtab.table * Registrations.T Symtab.table;
    6.85      (* 1st entry: locale namespace,
    6.86 @@ -331,39 +331,37 @@
    6.87  
    6.88    val empty = (NameSpace.empty, Symtab.empty, Symtab.empty);
    6.89    val copy = I;
    6.90 -  val prep_ext = I;
    6.91 +  val extend = I;
    6.92  
    6.93 -  fun join_locs ({predicate, import, elems, params}: locale,
    6.94 +  fun join_locs _ ({predicate, import, elems, params}: locale,
    6.95        {elems = elems', ...}: locale) =
    6.96      SOME {predicate = predicate, import = import,
    6.97        elems = gen_merge_lists eq_snd elems elems',
    6.98        params = params};
    6.99 -  fun merge ((space1, locs1, regs1), (space2, locs2, regs2)) =
   6.100 +  fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
   6.101      (NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2),
   6.102 -     Symtab.join (SOME o Registrations.join) (regs1, regs2));
   6.103 +     Symtab.join (K (SOME o Registrations.join)) (regs1, regs2));
   6.104  
   6.105    fun print _ (space, locs, _) =
   6.106      Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
   6.107      |> Pretty.writeln;
   6.108 -end;
   6.109 +end);
   6.110  
   6.111 -structure GlobalLocalesData = TheoryDataFun(GlobalLocalesArgs);
   6.112  val _ = Context.add_setup [GlobalLocalesData.init];
   6.113  
   6.114  
   6.115  
   6.116  (** context data **)
   6.117  
   6.118 -structure LocalLocalesArgs =
   6.119 -struct
   6.120 +structure LocalLocalesData = ProofDataFun
   6.121 +(struct
   6.122    val name = "Isar/locales";
   6.123    type T = Registrations.T Symtab.table;
   6.124      (* registrations, indexed by locale name *)
   6.125    fun init _ = Symtab.empty;
   6.126    fun print _ _ = ();
   6.127 -end;
   6.128 +end);
   6.129  
   6.130 -structure LocalLocalesData = ProofDataFun(LocalLocalesArgs);
   6.131  val _ = Context.add_setup [LocalLocalesData.init];
   6.132  
   6.133  
   6.134 @@ -371,12 +369,12 @@
   6.135  
   6.136  val print_locales = GlobalLocalesData.print;
   6.137  
   6.138 -val intern = NameSpace.intern o #1 o GlobalLocalesData.get_sg;
   6.139 -val extern = NameSpace.extern o #1 o GlobalLocalesData.get_sg;
   6.140 +val intern = NameSpace.intern o #1 o GlobalLocalesData.get;
   6.141 +val extern = NameSpace.extern o #1 o GlobalLocalesData.get;
   6.142  
   6.143  fun declare_locale name thy =
   6.144    thy |> GlobalLocalesData.map (fn (space, locs, regs) =>
   6.145 -    (Sign.declare_name (Theory.sign_of thy) name space, locs, regs));
   6.146 +    (Sign.declare_name thy name space, locs, regs));
   6.147  
   6.148  fun put_locale name loc =
   6.149    GlobalLocalesData.map (fn (space, locs, regs) =>
   6.150 @@ -408,15 +406,15 @@
   6.151  val get_local_registrations =
   6.152       gen_get_registrations LocalLocalesData.get;
   6.153  
   6.154 -fun gen_get_registration get get_sg thy_ctxt (name, ps) =
   6.155 +fun gen_get_registration get thy_of thy_ctxt (name, ps) =
   6.156    case Symtab.lookup (get thy_ctxt, name) of
   6.157        NONE => NONE
   6.158 -    | SOME reg => Registrations.lookup (get_sg thy_ctxt) (reg, ps);
   6.159 +    | SOME reg => Registrations.lookup (thy_of thy_ctxt) (reg, ps);
   6.160  
   6.161  val get_global_registration =
   6.162 -     gen_get_registration (#3 o GlobalLocalesData.get) Theory.sign_of;
   6.163 +     gen_get_registration (#3 o GlobalLocalesData.get) I;
   6.164  val get_local_registration =
   6.165 -     gen_get_registration LocalLocalesData.get ProofContext.sign_of;
   6.166 +     gen_get_registration LocalLocalesData.get ProofContext.theory_of;
   6.167  
   6.168  val test_global_registration = isSome oo get_global_registration;
   6.169  val test_local_registration = isSome oo get_local_registration;
   6.170 @@ -430,15 +428,15 @@
   6.171  
   6.172  (* add registration to theory or context, ignored if subsumed *)
   6.173  
   6.174 -fun gen_put_registration map_data get_sg (name, ps) attn thy_ctxt =
   6.175 +fun gen_put_registration map_data thy_of (name, ps) attn thy_ctxt =
   6.176    map_data (fn regs =>
   6.177      let
   6.178 -      val sg = get_sg thy_ctxt;
   6.179 +      val thy = thy_of thy_ctxt;
   6.180        val reg = getOpt (Symtab.lookup (regs, name), Registrations.empty);
   6.181 -      val (reg', sups) = Registrations.insert sg (ps, attn) reg;
   6.182 +      val (reg', sups) = Registrations.insert thy (ps, attn) reg;
   6.183        val _ = if not (null sups) then warning
   6.184                  ("Subsumed interpretation(s) of locale " ^
   6.185 -                 quote (extern sg name) ^
   6.186 +                 quote (extern thy name) ^
   6.187                   "\nby interpretation(s) with the following prefix(es):\n" ^
   6.188                    commas_quote (map (fn (_, ((s, _), _)) => s) sups))
   6.189                else ();
   6.190 @@ -446,10 +444,9 @@
   6.191  
   6.192  val put_global_registration =
   6.193       gen_put_registration (fn f =>
   6.194 -       GlobalLocalesData.map (fn (space, locs, regs) =>
   6.195 -         (space, locs, f regs))) Theory.sign_of;
   6.196 +       GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, f regs))) I;
   6.197  val put_local_registration =
   6.198 -     gen_put_registration LocalLocalesData.map ProofContext.sign_of;
   6.199 +     gen_put_registration LocalLocalesData.map ProofContext.theory_of;
   6.200  
   6.201  (* TODO: needed? *)
   6.202  (*
   6.203 @@ -487,7 +484,6 @@
   6.204  
   6.205  fun imports thy (upper, lower) =
   6.206    let
   6.207 -    val sign = sign_of thy;
   6.208      fun imps (Locale name) low = (name = low) orelse
   6.209        (case get_locale thy name of
   6.210             NONE => false
   6.211 @@ -495,7 +491,7 @@
   6.212        | imps (Rename (expr, _)) low = imps expr low
   6.213        | imps (Merge es) low = exists (fn e => imps e low) es;
   6.214    in
   6.215 -    imps (Locale (intern sign upper)) (intern sign lower)
   6.216 +    imps (Locale (intern thy upper)) (intern thy lower)
   6.217    end;
   6.218  
   6.219  
   6.220 @@ -505,7 +501,6 @@
   6.221    let
   6.222      val ctxt = mk_ctxt thy_ctxt;
   6.223      val thy = ProofContext.theory_of ctxt;
   6.224 -    val sg = Theory.sign_of thy;
   6.225  
   6.226      val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
   6.227      val prt_atts = Args.pretty_attribs ctxt;
   6.228 @@ -517,7 +512,7 @@
   6.229                [Pretty.str ":", Pretty.brk 1,
   6.230                  Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts))]));
   6.231  
   6.232 -    val loc_int = intern sg loc;
   6.233 +    val loc_int = intern thy loc;
   6.234      val regs = get_regs thy_ctxt;
   6.235      val loc_regs = Symtab.lookup (regs, loc_int);
   6.236    in
   6.237 @@ -547,9 +542,9 @@
   6.238  
   6.239  fun err_in_locale ctxt msg ids =
   6.240    let
   6.241 -    val sign = ProofContext.sign_of ctxt;
   6.242 +    val thy = ProofContext.theory_of ctxt;
   6.243      fun prt_id (name, parms) =
   6.244 -      [Pretty.block (Pretty.breaks (map Pretty.str (extern sign name :: parms)))];
   6.245 +      [Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))];
   6.246      val prt_ids = List.concat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids));
   6.247      val err_msg =
   6.248        if forall (equal "" o #1) ids then msg
   6.249 @@ -591,7 +586,7 @@
   6.250  
   6.251  fun map_attrib_elem f = map_elem {name = I, var = I, typ = I, term = I, fact = I, attrib = f};
   6.252  
   6.253 -fun intern_attrib_elem thy = map_attrib_elem (Attrib.intern_src (Theory.sign_of thy));
   6.254 +fun intern_attrib_elem thy = map_attrib_elem (Attrib.intern_src thy);
   6.255  
   6.256  fun intern_attrib_elem_expr thy (Elem elem) = Elem (intern_attrib_elem thy elem)
   6.257    | intern_attrib_elem_expr _ (Expr expr) = Expr expr;
   6.258 @@ -623,8 +618,8 @@
   6.259  
   6.260  fun rename_thm ren th =
   6.261    let
   6.262 -    val {sign, hyps, prop, maxidx, ...} = Thm.rep_thm th;
   6.263 -    val cert = Thm.cterm_of sign;
   6.264 +    val {thy, hyps, prop, maxidx, ...} = Thm.rep_thm th;
   6.265 +    val cert = Thm.cterm_of thy;
   6.266      val (xs, Ts) = Library.split_list (Library.foldl Term.add_frees ([], prop :: hyps));
   6.267      val xs' = map (rename ren) xs;
   6.268      fun cert_frees names = map (cert o Free) (names ~~ Ts);
   6.269 @@ -659,9 +654,9 @@
   6.270  fun inst_thm _ [] th = th
   6.271    | inst_thm ctxt env th =
   6.272        let
   6.273 -        val sign = ProofContext.sign_of ctxt;
   6.274 -        val cert = Thm.cterm_of sign;
   6.275 -        val certT = Thm.ctyp_of sign;
   6.276 +        val thy = ProofContext.theory_of ctxt;
   6.277 +        val cert = Thm.cterm_of thy;
   6.278 +        val certT = Thm.ctyp_of thy;
   6.279          val {hyps, prop, maxidx, ...} = Thm.rep_thm th;
   6.280          val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
   6.281          val env' = List.filter (fn ((a, _), _) => a mem_string tfrees) env;
   6.282 @@ -686,16 +681,16 @@
   6.283  
   6.284  (* instantiate TFrees *)
   6.285  
   6.286 -fun tinst_tab_elem sg tinst =
   6.287 -  map_values (tinst_tab_type tinst) (tinst_tab_term tinst) (tinst_tab_thm sg tinst);
   6.288 +fun tinst_tab_elem thy tinst =
   6.289 +  map_values (tinst_tab_type tinst) (tinst_tab_term tinst) (tinst_tab_thm thy tinst);
   6.290  
   6.291  (* instantiate TFrees and Frees *)
   6.292  
   6.293 -fun inst_tab_elem sg (inst as (_, tinst)) =
   6.294 -  map_values (tinst_tab_type tinst) (inst_tab_term inst) (inst_tab_thm sg inst);
   6.295 +fun inst_tab_elem thy (inst as (_, tinst)) =
   6.296 +  map_values (tinst_tab_type tinst) (inst_tab_term inst) (inst_tab_thm thy inst);
   6.297  
   6.298 -fun inst_tab_elems sign inst ((n, ps), elems) =
   6.299 -      ((n, map (inst_tab_term inst) ps), map (inst_tab_elem sign inst) elems);
   6.300 +fun inst_tab_elems thy inst ((n, ps), elems) =
   6.301 +      ((n, map (inst_tab_term inst) ps), map (inst_tab_elem thy inst) elems);
   6.302  
   6.303  
   6.304  (** structured contexts: rename + merge + implicit type instantiation **)
   6.305 @@ -719,7 +714,7 @@
   6.306  
   6.307      val (maxidx', Ts') = foldl_map paramify (maxidx, Ts);
   6.308      val (maxidx'', Us') = foldl_map paramify (maxidx', Us);
   6.309 -    val tsig = Sign.tsig_of (ProofContext.sign_of ctxt);
   6.310 +    val tsig = Sign.tsig_of (ProofContext.theory_of ctxt);
   6.311  
   6.312      fun unify (env, (SOME T, SOME U)) = (Type.unify tsig env (U, T)
   6.313            handle Type.TUNIFY =>
   6.314 @@ -771,8 +766,8 @@
   6.315  fun unify_parms ctxt (fixed_parms : (string * typ) list)
   6.316    (raw_parmss : (string * typ option) list list) =
   6.317    let
   6.318 -    val sign = ProofContext.sign_of ctxt;
   6.319 -    val tsig = Sign.tsig_of sign;
   6.320 +    val thy = ProofContext.theory_of ctxt;
   6.321 +    val tsig = Sign.tsig_of thy;
   6.322      val maxidx = length raw_parmss;
   6.323      val idx_parmss = (0 upto maxidx - 1) ~~ raw_parmss;
   6.324  
   6.325 @@ -783,7 +778,7 @@
   6.326      fun unify T ((env, maxidx), U) =
   6.327        Type.unify tsig (env, maxidx) (U, T)
   6.328        handle Type.TUNIFY =>
   6.329 -        let val prt = Sign.string_of_typ sign
   6.330 +        let val prt = Sign.string_of_typ thy
   6.331          in raise TYPE ("unify_parms: failed to unify types " ^
   6.332            prt U ^ " and " ^ prt T, [U, T], [])
   6.333          end
   6.334 @@ -1065,9 +1060,9 @@
   6.335  
   6.336  (* expressions *)
   6.337  
   6.338 -fun intern_expr sg (Locale xname) = Locale (intern sg xname)
   6.339 -  | intern_expr sg (Merge exprs) = Merge (map (intern_expr sg) exprs)
   6.340 -  | intern_expr sg (Rename (expr, xs)) = Rename (intern_expr sg expr, xs);
   6.341 +fun intern_expr thy (Locale xname) = Locale (intern thy xname)
   6.342 +  | intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs)
   6.343 +  | intern_expr thy (Rename (expr, xs)) = Rename (intern_expr thy expr, xs);
   6.344  
   6.345  
   6.346  (* parameters *)
   6.347 @@ -1196,14 +1191,14 @@
   6.348      val eq' = Term.list_abs_free (map Term.dest_Free xs, rhs);
   6.349    in (Term.dest_Free f, eq') end;
   6.350  
   6.351 -fun abstract_thm sign eq =
   6.352 -  Thm.assume (Thm.cterm_of sign eq) |> Drule.gen_all |> Drule.abs_def;
   6.353 +fun abstract_thm thy eq =
   6.354 +  Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;
   6.355  
   6.356  fun bind_def ctxt (name, ps) ((xs, env, ths), eq) =
   6.357    let
   6.358      val ((y, T), b) = abstract_term eq;
   6.359      val b' = norm_term env b;
   6.360 -    val th = abstract_thm (ProofContext.sign_of ctxt) eq;
   6.361 +    val th = abstract_thm (ProofContext.theory_of ctxt) eq;
   6.362      fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];
   6.363    in
   6.364      conditional (exists (equal y o #1) xs) (fn () =>
   6.365 @@ -1382,7 +1377,7 @@
   6.366       {var = I, typ = I, term = I,
   6.367        name = prep_name ctxt,
   6.368        fact = get ctxt,
   6.369 -      attrib = Args.assignable o intern (ProofContext.sign_of ctxt)};
   6.370 +      attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
   6.371  
   6.372  in
   6.373  
   6.374 @@ -1399,11 +1394,12 @@
   6.375  fun prep_context_statement prep_expr prep_elemss prep_facts
   6.376      do_close fixed_params import elements raw_concl context =
   6.377    let
   6.378 -    val sign = ProofContext.sign_of context;
   6.379 +    val thy = ProofContext.theory_of context;
   6.380  
   6.381 -    val ((import_ids, import_syn), raw_import_elemss) = flatten (context, prep_expr sign) (([], Symtab.empty), Expr import);
   6.382 +    val ((import_ids, import_syn), raw_import_elemss) =
   6.383 +      flatten (context, prep_expr thy) (([], Symtab.empty), Expr import);
   6.384      (* CB: normalise "includes" among elements *)
   6.385 -    val ((ids, syn), raw_elemsss) = foldl_map (flatten (context, prep_expr sign))
   6.386 +    val ((ids, syn), raw_elemsss) = foldl_map (flatten (context, prep_expr thy))
   6.387        ((import_ids, import_syn), elements);
   6.388  
   6.389      val raw_elemss = List.concat raw_elemsss;
   6.390 @@ -1426,7 +1422,7 @@
   6.391      val stmt = gen_distinct Term.aconv
   6.392         (List.concat (map (fn ((_, axs), _) =>
   6.393           List.concat (map (#hyps o Thm.rep_thm) axs)) qs));
   6.394 -    val cstmt = map (cterm_of sign) stmt;
   6.395 +    val cstmt = map (cterm_of thy) stmt;
   6.396    in
   6.397      ((((import_ctxt, import_elemss), (ctxt, elemss, syn)), (parms, spec, defs)), (cstmt, concl))
   6.398    end;
   6.399 @@ -1437,7 +1433,7 @@
   6.400  fun gen_statement prep_locale prep_ctxt raw_locale elems concl ctxt =
   6.401    let
   6.402      val thy = ProofContext.theory_of ctxt;
   6.403 -    val locale = Option.map (prep_locale (Theory.sign_of thy)) raw_locale;
   6.404 +    val locale = Option.map (prep_locale thy) raw_locale;
   6.405      val (target_stmt, fixed_params, import) =
   6.406        (case locale of NONE => ([], [], empty)
   6.407        | SOME name =>
   6.408 @@ -1577,7 +1573,7 @@
   6.409      val (parms, parmTs_o) =
   6.410            the_locale thy target |> #params |> fst |> map fst |> split_list;
   6.411      val parmvTs = map (Type.varifyT o valOf) parmTs_o;
   6.412 -    val ids = flatten (ProofContext.init thy, intern_expr (Theory.sign_of thy))
   6.413 +    val ids = flatten (ProofContext.init thy, intern_expr thy)
   6.414        (([], Symtab.empty), Expr (Locale target)) |> fst |> fst |> map fst;
   6.415  
   6.416      val regs = get_global_registrations thy target;
   6.417 @@ -1586,10 +1582,9 @@
   6.418  
   6.419      fun activate (thy, (vts, ((prfx, atts2), _))) =
   6.420        let
   6.421 -        val sg = Theory.sign_of thy;
   6.422          val ts = map Logic.unvarify vts;
   6.423          (* type instantiation *)
   6.424 -        val vtinst = Library.foldl (Type.typ_match (Sign.tsig_of sg))
   6.425 +        val vtinst = Library.foldl (Type.typ_match (Sign.tsig_of thy))
   6.426               (Vartab.empty, (parmvTs ~~ map Term.fastype_of ts));
   6.427          val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T))
   6.428               |> Symtab.make;            
   6.429 @@ -1602,7 +1597,7 @@
   6.430          val args' = map (fn ((n, atts), [(ths, [])]) =>
   6.431              ((if prfx = "" orelse n = "" then "" else NameSpace.pack [prfx, n],  (* FIXME *)
   6.432                map (Attrib.global_attribute_i thy) (atts @ atts2)),
   6.433 -             [(map (Drule.standard o Drule.satisfy_hyps prems o inst_tab_thm sg (inst, tinst)) ths, [])]))
   6.434 +             [(map (Drule.standard o Drule.satisfy_hyps prems o inst_tab_thm thy (inst, tinst)) ths, [])]))
   6.435            args;
   6.436        in global_note_accesses_i (Drule.kind kind) prfx args' thy |> fst end;
   6.437    in Library.foldl activate (thy, regs) end;
   6.438 @@ -1632,7 +1627,7 @@
   6.439  fun gen_note_thmss prep_locale prep_facts kind raw_loc args thy =
   6.440    let
   6.441      val thy_ctxt = ProofContext.init thy;
   6.442 -    val loc = prep_locale (Theory.sign_of thy) raw_loc;
   6.443 +    val loc = prep_locale thy raw_loc;
   6.444      val (_, (stmt, _), loc_ctxt, _, _) = cert_context_statement (SOME loc) [] [] thy_ctxt;
   6.445      val export = ProofContext.export_standard stmt loc_ctxt thy_ctxt;
   6.446  
   6.447 @@ -1678,14 +1673,14 @@
   6.448  val introN = "intro";
   6.449  val axiomsN = "axioms";
   6.450  
   6.451 -fun atomize_spec sign ts =
   6.452 +fun atomize_spec thy ts =
   6.453    let
   6.454      val t = foldr1 Logic.mk_conjunction ts;
   6.455 -    val body = ObjectLogic.atomize_term sign t;
   6.456 +    val body = ObjectLogic.atomize_term thy t;
   6.457      val bodyT = Term.fastype_of body;
   6.458    in
   6.459 -    if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of sign t))
   6.460 -    else (body, bodyT, ObjectLogic.atomize_rule sign (Thm.cterm_of sign t))
   6.461 +    if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
   6.462 +    else (body, bodyT, ObjectLogic.atomize_rule thy (Thm.cterm_of thy t))
   6.463    end;
   6.464  
   6.465  fun aprop_tr' n c = (c, fn args =>
   6.466 @@ -1703,10 +1698,9 @@
   6.467  
   6.468  fun def_pred bname parms defs ts norm_ts thy =
   6.469    let
   6.470 -    val sign = Theory.sign_of thy;
   6.471 -    val name = Sign.full_name sign bname;
   6.472 +    val name = Sign.full_name thy bname;
   6.473  
   6.474 -    val (body, bodyT, body_eq) = atomize_spec sign norm_ts;
   6.475 +    val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
   6.476      val env = Term.add_term_free_names (body, []);
   6.477      val xs = List.filter (fn (x, _) => x mem_string env) parms;
   6.478      val Ts = map #2 xs;
   6.479 @@ -1716,7 +1710,7 @@
   6.480  
   6.481      val args = map Logic.mk_type extraTs @ map Free xs;
   6.482      val head = Term.list_comb (Const (name, predT), args);
   6.483 -    val statement = ObjectLogic.assert_propT sign head;
   6.484 +    val statement = ObjectLogic.assert_propT thy head;
   6.485  
   6.486      val (defs_thy, [pred_def]) =
   6.487        thy
   6.488 @@ -1725,10 +1719,9 @@
   6.489        |> Theory.add_consts_i [(bname, predT, Syntax.NoSyn)]
   6.490        |> PureThy.add_defs_i false [((Thm.def_name bname, Logic.mk_equals (head, body)), [])];
   6.491  
   6.492 -    val defs_sign = Theory.sign_of defs_thy;
   6.493 -    val cert = Thm.cterm_of defs_sign;
   6.494 +    val cert = Thm.cterm_of defs_thy;
   6.495  
   6.496 -    val intro = Tactic.prove_standard defs_sign [] norm_ts statement (fn _ =>
   6.497 +    val intro = Tactic.prove_standard defs_thy [] norm_ts statement (fn _ =>
   6.498        Tactic.rewrite_goals_tac [pred_def] THEN
   6.499        Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
   6.500        Tactic.compose_tac (false, Drule.conj_intr_list (map (Thm.assume o cert) norm_ts), 0) 1);
   6.501 @@ -1738,7 +1731,7 @@
   6.502          Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))]
   6.503        |> Drule.conj_elim_precise (length ts);
   6.504      val axioms = (ts ~~ conjuncts) |> map (fn (t, ax) =>
   6.505 -      Tactic.prove_plain defs_sign [] [] t (fn _ =>
   6.506 +      Tactic.prove_plain defs_thy [] [] t (fn _ =>
   6.507          Tactic.rewrite_goals_tac defs THEN
   6.508          Tactic.compose_tac (false, ax, 0) 1));
   6.509    in (defs_thy, (statement, intro, axioms)) end;
   6.510 @@ -1788,7 +1781,7 @@
   6.511          let
   6.512            val (def_thy, (statement, intro, axioms)) =
   6.513              thy' |> def_pred bname parms defs (ints @ more_ts) (ints' @ more_ts);
   6.514 -          val cstatement = Thm.cterm_of (Theory.sign_of def_thy) statement;
   6.515 +          val cstatement = Thm.cterm_of def_thy statement;
   6.516          in
   6.517            def_thy |> note_thmss_qualified "" bname
   6.518              [((introN, []), [([intro], [])]),
   6.519 @@ -1808,8 +1801,7 @@
   6.520    (* CB: do_pred controls generation of predicates.
   6.521           true -> with, false -> without predicates. *)
   6.522    let
   6.523 -    val sign = Theory.sign_of thy;
   6.524 -    val name = Sign.full_name sign bname;
   6.525 +    val name = Sign.full_name thy bname;
   6.526      val _ = conditional (isSome (get_locale thy name)) (fn () =>
   6.527        error ("Duplicate definition of locale " ^ quote name));
   6.528  
   6.529 @@ -1817,6 +1809,7 @@
   6.530      val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)), text) =
   6.531        prep_ctxt raw_import raw_body thy_ctxt;
   6.532      val elemss = import_elemss @ body_elemss;
   6.533 +    val import = prep_expr thy raw_import;
   6.534  
   6.535      val (pred_thy, (elemss', predicate as (predicate_statement, predicate_axioms))) =
   6.536        if do_pred then thy |> define_preds bname text elemss
   6.537 @@ -1838,7 +1831,7 @@
   6.538      pred_thy
   6.539      |> note_thmss_qualified "" name facts' |> #1
   6.540      |> declare_locale name
   6.541 -    |> put_locale name {predicate = predicate, import = prep_expr sign raw_import,
   6.542 +    |> put_locale name {predicate = predicate, import = import,
   6.543          elems = map (fn e => (e, stamp ())) (List.concat (map #2 (List.filter (equal "" o #1 o #1) elemss'))),
   6.544          params = (params_of elemss' |>
   6.545            map (fn (x, T) => ((x, T), valOf (Symtab.lookup (syn, x)))), map #1 (params_of body_elemss))}
   6.546 @@ -1935,10 +1928,10 @@
   6.547      attn expr insts thy_ctxt =
   6.548    let
   6.549      val ctxt = mk_ctxt thy_ctxt;
   6.550 -    val sign = ProofContext.sign_of ctxt;
   6.551 +    val thy = ProofContext.theory_of ctxt;
   6.552  
   6.553      val ctxt' = ctxt |> ProofContext.theory_of |> ProofContext.init;
   6.554 -    val ((ids, _), raw_elemss) = flatten (ctxt', intern_expr sign)
   6.555 +    val ((ids, _), raw_elemss) = flatten (ctxt', intern_expr thy)
   6.556            (([], Symtab.empty), Expr expr);
   6.557      val do_close = false;  (* effect unknown *)
   6.558      val ((parms, all_elemss, _), (spec, (xs, defs, _))) =
   6.559 @@ -2004,7 +1997,7 @@
   6.560  
   6.561      (* instantiate ids and elements *)
   6.562      val inst_elemss = map
   6.563 -          (fn (id, (_, elems)) => inst_tab_elems sign (inst, tinst) (id, 
   6.564 +          (fn (id, (_, elems)) => inst_tab_elems thy (inst, tinst) (id, 
   6.565              map (fn Int e => e) elems)) 
   6.566            (ids' ~~ all_elemss);
   6.567  
   6.568 @@ -2016,7 +2009,7 @@
   6.569      val propss = extract_asms_elemss new_inst_elemss;
   6.570  
   6.571      val bind_attrib = Attrib.crude_closure ctxt o Args.assignable;
   6.572 -    val attn' = apsnd (map (bind_attrib o Attrib.intern_src sign)) attn;
   6.573 +    val attn' = apsnd (map (bind_attrib o Attrib.intern_src thy)) attn;
   6.574  
   6.575      (** add registrations to theory or context,
   6.576          without theorems, these are added after the proof **)
   6.577 @@ -2034,7 +2027,7 @@
   6.578  val prep_global_registration = gen_prep_registration
   6.579       ProofContext.init false
   6.580       (fn thy => fn sorts => fn used =>
   6.581 -       Sign.read_def_terms (Theory.sign_of thy, K NONE, sorts) used true)
   6.582 +       Sign.read_def_terms (thy, K NONE, sorts) used true)
   6.583       (fn thy => fn (name, ps) =>
   6.584         test_global_registration thy (name, map Logic.varify ps))
   6.585       (fn (name, ps) => put_global_registration (name, map Logic.varify ps))
     7.1 --- a/src/Pure/Isar/proof_context.ML	Fri Jun 17 18:33:42 2005 +0200
     7.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Jun 17 18:35:27 2005 +0200
     7.3 @@ -13,7 +13,7 @@
     7.4    type exporter
     7.5    exception CONTEXT of string * context
     7.6    val theory_of: context -> theory
     7.7 -  val sign_of: context -> Sign.sg
     7.8 +  val sign_of: context -> theory    (*obsolete*)
     7.9    val is_fixed: context -> string -> bool
    7.10    val is_known: context -> string -> bool
    7.11    val fixed_names_of: context -> string list
    7.12 @@ -198,7 +198,7 @@
    7.13    make_context (f (thy, syntax, data, asms, binds, thms, cases, defs));
    7.14  
    7.15  fun theory_of (Context {thy, ...}) = thy;
    7.16 -val sign_of = Theory.sign_of o theory_of;
    7.17 +val sign_of = theory_of;
    7.18  fun syntax_of (Context {syntax, ...}) = syntax;
    7.19  
    7.20  fun fixes_of (Context {asms = (_, fixes), ...}) = fixes;
    7.21 @@ -218,7 +218,7 @@
    7.22  
    7.23  (* errors *)
    7.24  
    7.25 -fun of_theory thy = "\nof theory " ^ Sign.str_of_sg (Theory.sign_of thy);
    7.26 +fun of_theory thy = "\nof theory " ^ Context.str_of_thy thy;
    7.27  
    7.28  fun err_inconsistent kinds =
    7.29    error ("Attempt to merge different versions of " ^ commas_quote kinds ^ " proof data");
    7.30 @@ -240,20 +240,19 @@
    7.31  
    7.32  (* data kind 'Isar/proof_data' *)
    7.33  
    7.34 -structure ProofDataDataArgs =
    7.35 -struct
    7.36 +structure ProofDataData = TheoryDataFun
    7.37 +(struct
    7.38    val name = "Isar/proof_data";
    7.39    type T = (Object.kind * ((theory -> Object.T) * (context -> Object.T -> unit))) Symtab.table;
    7.40  
    7.41    val empty = Symtab.empty;
    7.42    val copy = I;
    7.43 -  val prep_ext = I;
    7.44 -  fun merge tabs = Symtab.merge (Object.eq_kind o pairself fst) tabs
    7.45 +  val extend = I;
    7.46 +  fun merge _ tabs = Symtab.merge (Object.eq_kind o pairself fst) tabs
    7.47      handle Symtab.DUPS kinds => err_inconsistent kinds;
    7.48    fun print _ tab = Pretty.writeln (Pretty.strs (map #1 (Symtab.dest tab)));
    7.49 -end;
    7.50 +end);
    7.51  
    7.52 -structure ProofDataData = TheoryDataFun(ProofDataDataArgs);
    7.53  val _ = Context.add_setup [ProofDataData.init];
    7.54  val print_proof_data = ProofDataData.print;
    7.55  
    7.56 @@ -304,7 +303,7 @@
    7.57  
    7.58  fun init thy =
    7.59    let val data = Symtab.map (fn (_, (f, _)) => f thy) (ProofDataData.get thy) in
    7.60 -    make_context (thy, (Theory.syn_of thy, [], []), data, (([], []), []), Vartab.empty,
    7.61 +    make_context (thy, (Sign.syn_of thy, [], []), data, (([], []), []), Vartab.empty,
    7.62        (NameSpace.default_naming, NameSpace.empty_table, FactIndex.empty), [],
    7.63        (Vartab.empty, Vartab.empty, [], Symtab.empty))
    7.64    end;
    7.65 @@ -364,7 +363,7 @@
    7.66  fun add_syntax decls =
    7.67    map_context (fn (thy, (syn, structs, mixfixed), data, asms, binds, thms, cases, defs) =>
    7.68      let
    7.69 -      val is_logtype = Sign.is_logtype (Theory.sign_of thy);
    7.70 +      val is_logtype = Sign.is_logtype thy;
    7.71        val structs' = structs @ List.mapPartial prep_struct decls;
    7.72        val mxs = List.mapPartial prep_mixfix decls;
    7.73        val (fixed, mxs_output) = Library.split_list (List.mapPartial prep_mixfix' decls);
    7.74 @@ -385,11 +384,11 @@
    7.75  
    7.76  (** pretty printing **)
    7.77  
    7.78 -fun pretty_term ctxt t = Sign.pretty_term' (syn_of ctxt) (sign_of ctxt) (context_tr' ctxt t);
    7.79 -fun pretty_typ ctxt T = Sign.pretty_typ (sign_of ctxt) T;
    7.80 -fun pretty_sort ctxt S = Sign.pretty_sort (sign_of ctxt) S;
    7.81 -fun pretty_classrel ctxt cs = Sign.pretty_classrel (sign_of ctxt) cs;
    7.82 -fun pretty_arity ctxt ar = Sign.pretty_arity (sign_of ctxt) ar;
    7.83 +fun pretty_term ctxt t = Sign.pretty_term' (syn_of ctxt) (theory_of ctxt) (context_tr' ctxt t);
    7.84 +fun pretty_typ ctxt T = Sign.pretty_typ (theory_of ctxt) T;
    7.85 +fun pretty_sort ctxt S = Sign.pretty_sort (theory_of ctxt) S;
    7.86 +fun pretty_classrel ctxt cs = Sign.pretty_classrel (theory_of ctxt) cs;
    7.87 +fun pretty_arity ctxt ar = Sign.pretty_arity (theory_of ctxt) ar;
    7.88  
    7.89  fun pp ctxt = Pretty.pp (pretty_term ctxt, pretty_typ ctxt, pretty_sort ctxt,
    7.90    pretty_classrel ctxt, pretty_arity ctxt);
    7.91 @@ -433,11 +432,11 @@
    7.92  local
    7.93  
    7.94  fun read_typ_aux read ctxt s =
    7.95 -  transform_error (read (syn_of ctxt) (sign_of ctxt, def_sort ctxt)) s
    7.96 +  transform_error (read (syn_of ctxt) (theory_of ctxt, def_sort ctxt)) s
    7.97      handle ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt);
    7.98  
    7.99  fun cert_typ_aux cert ctxt raw_T =
   7.100 -  cert (sign_of ctxt) raw_T
   7.101 +  cert (theory_of ctxt) raw_T
   7.102      handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt);
   7.103  
   7.104  in
   7.105 @@ -505,29 +504,29 @@
   7.106  
   7.107  (* read / certify wrt. signature *)     (*exception ERROR*) (*exception TERM*)
   7.108  
   7.109 -fun read_def_termTs freeze pp syn sg (types, sorts, used) sTs =
   7.110 -  Sign.read_def_terms' pp (Sign.is_logtype sg) syn (sg, types, sorts) used freeze sTs;
   7.111 +fun read_def_termTs freeze pp syn thy (types, sorts, used) sTs =
   7.112 +  Sign.read_def_terms' pp (Sign.is_logtype thy) syn (thy, types, sorts) used freeze sTs;
   7.113  
   7.114 -fun read_def_termT freeze pp syn sg defs sT =
   7.115 -  apfst hd (read_def_termTs freeze pp syn sg defs [sT]);
   7.116 +fun read_def_termT freeze pp syn thy defs sT =
   7.117 +  apfst hd (read_def_termTs freeze pp syn thy defs [sT]);
   7.118  
   7.119 -fun read_term_sg freeze pp syn sg defs s =
   7.120 -  #1 (read_def_termT freeze pp syn sg defs (s, TypeInfer.logicT));
   7.121 +fun read_term_thy freeze pp syn thy defs s =
   7.122 +  #1 (read_def_termT freeze pp syn thy defs (s, TypeInfer.logicT));
   7.123  
   7.124 -fun read_prop_sg freeze pp syn sg defs s =
   7.125 -  #1 (read_def_termT freeze pp syn sg defs (s, propT));
   7.126 +fun read_prop_thy freeze pp syn thy defs s =
   7.127 +  #1 (read_def_termT freeze pp syn thy defs (s, propT));
   7.128  
   7.129 -fun read_terms_sg freeze pp syn sg defs =
   7.130 -  #1 o read_def_termTs freeze pp syn sg defs o map (rpair TypeInfer.logicT);
   7.131 +fun read_terms_thy freeze pp syn thy defs =
   7.132 +  #1 o read_def_termTs freeze pp syn thy defs o map (rpair TypeInfer.logicT);
   7.133  
   7.134 -fun read_props_sg freeze pp syn sg defs =
   7.135 -  #1 o read_def_termTs freeze pp syn sg defs o map (rpair propT);
   7.136 +fun read_props_thy freeze pp syn thy defs =
   7.137 +  #1 o read_def_termTs freeze pp syn thy defs o map (rpair propT);
   7.138  
   7.139  
   7.140 -fun cert_term_sg pp sg t = #1 (Sign.certify_term pp sg t);
   7.141 +fun cert_term_thy pp thy t = #1 (Sign.certify_term pp thy t);
   7.142  
   7.143 -fun cert_prop_sg pp sg tm =
   7.144 -  let val (t, T, _) = Sign.certify_term pp sg tm
   7.145 +fun cert_prop_thy pp thy tm =
   7.146 +  let val (t, T, _) = Sign.certify_term pp thy tm
   7.147    in if T = propT then t else raise TERM ("Term not of type prop", [t]) end;
   7.148  
   7.149  
   7.150 @@ -538,7 +537,7 @@
   7.151  
   7.152  fun unifyT ctxt (T, U) =
   7.153    let val maxidx = Int.max (Term.maxidx_of_typ T, Term.maxidx_of_typ U)
   7.154 -  in #1 (Type.unify (Sign.tsig_of (sign_of ctxt)) (Vartab.empty, maxidx) (T, U)) end;
   7.155 +  in #1 (Type.unify (Sign.tsig_of (theory_of ctxt)) (Vartab.empty, maxidx) (T, U)) end;
   7.156  
   7.157  fun norm_term (ctxt as Context {binds, ...}) schematic =
   7.158    let
   7.159 @@ -588,7 +587,7 @@
   7.160      val sorts = append_env (def_sort ctxt) more_sorts;
   7.161      val used = used_types ctxt @ more_used;
   7.162    in
   7.163 -    (transform_error (read (pp ctxt) (syn_of ctxt) (sign_of ctxt) (types, sorts, used)) s
   7.164 +    (transform_error (read (pp ctxt) (syn_of ctxt) (theory_of ctxt) (types, sorts, used)) s
   7.165        handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
   7.166          | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
   7.167      |> app (intern_skolem ctxt internal)
   7.168 @@ -609,13 +608,13 @@
   7.169  val read_prop_pats = read_term_pats propT;
   7.170  
   7.171  fun read_term_liberal ctxt =
   7.172 -  gen_read' (read_term_sg true) I false false ctxt (K true) (K NONE) (K NONE) [];
   7.173 +  gen_read' (read_term_thy true) I false false ctxt (K true) (K NONE) (K NONE) [];
   7.174  
   7.175 -val read_term              = gen_read (read_term_sg true) I false false;
   7.176 -val read_prop              = gen_read (read_prop_sg true) I false false;
   7.177 -val read_prop_schematic    = gen_read (read_prop_sg true) I false true;
   7.178 -val read_terms             = gen_read (read_terms_sg true) map false false;
   7.179 -fun read_props schematic   = gen_read (read_props_sg true) map false schematic;
   7.180 +val read_term              = gen_read (read_term_thy true) I false false;
   7.181 +val read_prop              = gen_read (read_prop_thy true) I false false;
   7.182 +val read_prop_schematic    = gen_read (read_prop_thy true) I false true;
   7.183 +val read_terms             = gen_read (read_terms_thy true) map false false;
   7.184 +fun read_props schematic   = gen_read (read_props_thy true) map false schematic;
   7.185  
   7.186  end;
   7.187  
   7.188 @@ -626,17 +625,17 @@
   7.189  
   7.190  fun gen_cert cert pattern schematic ctxt t = t
   7.191    |> (if pattern then I else norm_term ctxt schematic)
   7.192 -  |> (fn t' => cert (pp ctxt) (sign_of ctxt) t'
   7.193 +  |> (fn t' => cert (pp ctxt) (theory_of ctxt) t'
   7.194      handle TERM (msg, _) => raise CONTEXT (msg, ctxt));
   7.195  
   7.196  in
   7.197  
   7.198 -val cert_term = gen_cert cert_term_sg false false;
   7.199 -val cert_prop = gen_cert cert_prop_sg false false;
   7.200 -val cert_props = map oo gen_cert cert_prop_sg false;
   7.201 +val cert_term = gen_cert cert_term_thy false false;
   7.202 +val cert_prop = gen_cert cert_prop_thy false false;
   7.203 +val cert_props = map oo gen_cert cert_prop_thy false;
   7.204  
   7.205 -fun cert_term_pats _ = map o gen_cert cert_term_sg true false;
   7.206 -val cert_prop_pats = map o gen_cert cert_prop_sg true false;
   7.207 +fun cert_term_pats _ = map o gen_cert cert_term_thy true false;
   7.208 +val cert_prop_pats = map o gen_cert cert_prop_thy true false;
   7.209  
   7.210  end;
   7.211  
   7.212 @@ -693,13 +692,13 @@
   7.213  
   7.214  fun read_tyname ctxt c =
   7.215    if c mem_string used_types ctxt then
   7.216 -    TFree (c, if_none (def_sort ctxt (c, ~1)) (Sign.defaultS (sign_of ctxt)))
   7.217 -  else Sign.read_tyname (sign_of ctxt) c;
   7.218 +    TFree (c, if_none (def_sort ctxt (c, ~1)) (Sign.defaultS (theory_of ctxt)))
   7.219 +  else Sign.read_tyname (theory_of ctxt) c;
   7.220  
   7.221  fun read_const ctxt c =
   7.222    (case lookup_skolem ctxt c of
   7.223      SOME c' => Free (c', dummyT)
   7.224 -  | NONE => Sign.read_const (sign_of ctxt) c);
   7.225 +  | NONE => Sign.read_const (theory_of ctxt) c);
   7.226  
   7.227  
   7.228  
   7.229 @@ -774,8 +773,8 @@
   7.230      |> Seq.map (Drule.implies_intr_list view)
   7.231      |> Seq.map (fn rule =>
   7.232        let
   7.233 -        val {sign, prop, ...} = Thm.rep_thm rule;
   7.234 -        val frees = map (Thm.cterm_of sign) (List.mapPartial (find_free prop) fixes);
   7.235 +        val {thy, prop, ...} = Thm.rep_thm rule;
   7.236 +        val frees = map (Thm.cterm_of thy) (List.mapPartial (find_free prop) fixes);
   7.237          val tfrees = gen (Term.add_term_tfree_names (prop, []));
   7.238        in
   7.239          rule
   7.240 @@ -852,7 +851,7 @@
   7.241  
   7.242          val maxidx = fold (fn (t1, t2) => fn i =>
   7.243            Int.max (Int.max (Term.maxidx_of_term t1, Term.maxidx_of_term t2), i)) pairs ~1;
   7.244 -        val envs = Unify.smash_unifiers (sign_of ctxt, Envir.empty maxidx,
   7.245 +        val envs = Unify.smash_unifiers (theory_of ctxt, Envir.empty maxidx,
   7.246            map swap pairs);    (*prefer assignment of variables from patterns*)
   7.247          val env =
   7.248            (case Seq.pull envs of
   7.249 @@ -882,7 +881,7 @@
   7.250  val add_binds = fold (gen_bind read_term);
   7.251  val add_binds_i = fold (gen_bind cert_term);
   7.252  
   7.253 -fun auto_bind f ts ctxt = ctxt |> add_binds_i (map drop_schematic (f (sign_of ctxt) ts));
   7.254 +fun auto_bind f ts ctxt = ctxt |> add_binds_i (map drop_schematic (f (theory_of ctxt) ts));
   7.255  val auto_bind_goal = auto_bind AutoBind.goal;
   7.256  val auto_bind_facts = auto_bind AutoBind.facts;
   7.257  
   7.258 @@ -977,12 +976,12 @@
   7.259  (*beware of proper order of evaluation!*)
   7.260  fun retrieve_thms f g (ctxt as Context {thy, thms = (_, (space, tab), _), ...}) =
   7.261    let
   7.262 -    val sg_ref = Sign.self_ref (Theory.sign_of thy);
   7.263 +    val thy_ref = Theory.self_ref thy;
   7.264      val get_from_thy = f thy;
   7.265    in
   7.266      fn xnamei as (xname, _) =>
   7.267        (case Symtab.lookup (tab, NameSpace.intern space xname) of
   7.268 -        SOME ths => map (Thm.transfer_sg (Sign.deref sg_ref)) (PureThy.select_thm xnamei ths)
   7.269 +        SOME ths => map (Thm.transfer (Theory.deref thy_ref)) (PureThy.select_thm xnamei ths)
   7.270        | _ => get_from_thy xnamei) |> g xname
   7.271    end;
   7.272  
   7.273 @@ -1116,7 +1115,7 @@
   7.274  
   7.275  fun head_of_def cprop =
   7.276    #1 (Term.strip_comb (#1 (Logic.dest_equals (Term.strip_all_body (Thm.term_of cprop)))))
   7.277 -  |> Thm.cterm_of (Thm.sign_of_cterm cprop);
   7.278 +  |> Thm.cterm_of (Thm.theory_of_cterm cprop);
   7.279  
   7.280  fun export_def _ cprops thm =
   7.281    thm
   7.282 @@ -1132,7 +1131,7 @@
   7.283  
   7.284  fun add_assm (ctxt, ((name, attrs), props)) =
   7.285    let
   7.286 -    val cprops = map (Thm.cterm_of (sign_of ctxt)) props;
   7.287 +    val cprops = map (Thm.cterm_of (theory_of ctxt)) props;
   7.288      val asms = map (Tactic.norm_hhf_rule o Thm.assume) cprops;
   7.289  
   7.290      val ths = map (fn th => ([th], [])) asms;
   7.291 @@ -1438,7 +1437,7 @@
   7.292  
   7.293      (*theory*)
   7.294      val pretty_thy = Pretty.block
   7.295 -      [Pretty.str "Theory:", Pretty.brk 1, Sign.pretty_sg (sign_of ctxt)];
   7.296 +      [Pretty.str "Theory:", Pretty.brk 1, Context.pretty_thy (theory_of ctxt)];
   7.297  
   7.298      (*defaults*)
   7.299      fun prt_atom prt prtT (x, X) = Pretty.block
     8.1 --- a/src/Pure/Proof/extraction.ML	Fri Jun 17 18:33:42 2005 +0200
     8.2 +++ b/src/Pure/Proof/extraction.ML	Fri Jun 17 18:35:27 2005 +0200
     8.3 @@ -7,7 +7,7 @@
     8.4  
     8.5  signature EXTRACTION =
     8.6  sig
     8.7 -  val set_preprocessor : (Sign.sg -> Proofterm.proof -> Proofterm.proof) -> theory -> theory
     8.8 +  val set_preprocessor : (theory -> Proofterm.proof -> Proofterm.proof) -> theory -> theory
     8.9    val add_realizes_eqns_i : ((term * term) list * (term * term)) list -> theory -> theory
    8.10    val add_realizes_eqns : string list -> theory -> theory
    8.11    val add_typeof_eqns_i : ((term * term) list * (term * term)) list -> theory -> theory
    8.12 @@ -86,9 +86,9 @@
    8.13    ({next, rs = rs1, net} : rules) ({next = next2, rs = rs2, ...} : rules) =
    8.14    foldr add_rule {next = next, rs = rs1, net = net} (rs2 \\ rs1);
    8.15  
    8.16 -fun condrew sign rules procs =
    8.17 +fun condrew thy rules procs =
    8.18    let
    8.19 -    val tsig = Sign.tsig_of sign;
    8.20 +    val tsig = Sign.tsig_of thy;
    8.21  
    8.22      fun rew tm =
    8.23        Pattern.rewrite_term tsig [] (condrew' :: procs) tm
    8.24 @@ -112,7 +112,7 @@
    8.25                (~1, map (Int.max o pairself maxidx_of_term) prems'),
    8.26               iTs = Tenv, asol = tenv};
    8.27            val env'' = Library.foldl (fn (env, p) =>
    8.28 -            Pattern.unify (sign, env, [pairself (lookup rew) p])) (env', prems')
    8.29 +            Pattern.unify (thy, env, [pairself (lookup rew) p])) (env', prems')
    8.30          in SOME (Envir.norm_term env'' (inc (ren tm2)))
    8.31          end handle Pattern.MATCH => NONE | Pattern.Unif => NONE)
    8.32            (sort (Int.compare o pairself fst)
    8.33 @@ -178,8 +178,8 @@
    8.34  
    8.35  (* data kind 'Pure/extraction' *)
    8.36  
    8.37 -structure ExtractionArgs =
    8.38 -struct
    8.39 +structure ExtractionData = TheoryDataFun
    8.40 +(struct
    8.41    val name = "Pure/extraction";
    8.42    type T =
    8.43      {realizes_eqns : rules,
    8.44 @@ -189,7 +189,7 @@
    8.45       realizers : (string list * (term * proof)) list Symtab.table,
    8.46       defs : thm list,
    8.47       expand : (string * term) list,
    8.48 -     prep : (Sign.sg -> proof -> proof) option}
    8.49 +     prep : (theory -> proof -> proof) option}
    8.50  
    8.51    val empty =
    8.52      {realizes_eqns = empty_rules,
    8.53 @@ -200,9 +200,9 @@
    8.54       expand = [],
    8.55       prep = NONE};
    8.56    val copy = I;
    8.57 -  val prep_ext = I;
    8.58 +  val extend = I;
    8.59  
    8.60 -  fun merge
    8.61 +  fun merge _
    8.62      (({realizes_eqns = realizes_eqns1, typeof_eqns = typeof_eqns1, types = types1,
    8.63         realizers = realizers1, defs = defs1, expand = expand1, prep = prep1},
    8.64        {realizes_eqns = realizes_eqns2, typeof_eqns = typeof_eqns2, types = types2,
    8.65 @@ -216,16 +216,15 @@
    8.66       expand = merge_lists expand1 expand2,
    8.67       prep = (case prep1 of NONE => prep2 | _ => prep1)};
    8.68  
    8.69 -  fun print sg (x : T) = ();
    8.70 -end;
    8.71 +  fun print _ _ = ();
    8.72 +end);
    8.73  
    8.74 -structure ExtractionData = TheoryDataFun(ExtractionArgs);
    8.75  val _ = Context.add_setup [ExtractionData.init];
    8.76  
    8.77  fun read_condeq thy =
    8.78 -  let val sg = sign_of (add_syntax thy)
    8.79 +  let val thy' = add_syntax thy
    8.80    in fn s =>
    8.81 -    let val t = Logic.varify (term_of (read_cterm sg (s, propT)))
    8.82 +    let val t = Logic.varify (term_of (read_cterm thy' (s, propT)))
    8.83      in (map Logic.dest_equals (Logic.strip_imp_prems t),
    8.84        Logic.dest_equals (Logic.strip_imp_concl t))
    8.85      end handle TERM _ => error ("Not a (conditional) meta equality:\n" ^ s)
    8.86 @@ -286,13 +285,13 @@
    8.87  fun freeze_thaw f x =
    8.88    map_term_types thaw (f (map_term_types freeze x));
    8.89  
    8.90 -fun etype_of sg vs Ts t =
    8.91 +fun etype_of thy vs Ts t =
    8.92    let
    8.93 -    val {typeof_eqns, ...} = ExtractionData.get_sg sg;
    8.94 +    val {typeof_eqns, ...} = ExtractionData.get thy;
    8.95      fun err () = error ("Unable to determine type of extracted program for\n" ^
    8.96 -      Sign.string_of_term sg t)
    8.97 -  in case strip_abs_body (freeze_thaw (condrew sg (#net typeof_eqns)
    8.98 -    [typeof_proc (Sign.defaultS sg) vs]) (list_abs (map (pair "x") (rev Ts),
    8.99 +      Sign.string_of_term thy t)
   8.100 +  in case strip_abs_body (freeze_thaw (condrew thy (#net typeof_eqns)
   8.101 +    [typeof_proc (Sign.defaultS thy) vs]) (list_abs (map (pair "x") (rev Ts),
   8.102        Const ("typeof", fastype_of1 (Ts, t) --> Type ("Type", [])) $ t))) of
   8.103        Const ("Type", _) $ u => (Logic.dest_type u handle TERM _ => err ())
   8.104      | _ => err ()
   8.105 @@ -319,28 +318,26 @@
   8.106      val rtypes = map fst types;
   8.107      val eqns = Net.merge (#net realizes_eqns, #net typeof_eqns, K false);
   8.108      val thy' = add_syntax thy;
   8.109 -    val sign = sign_of thy';
   8.110 -    val tsg = Sign.tsig_of sign;
   8.111      val rd = ProofSyntax.read_proof thy' false
   8.112    in fn (thm, (vs, s1, s2)) =>
   8.113      let
   8.114        val name = Thm.name_of_thm thm;
   8.115        val _ = assert (name <> "") "add_realizers: unnamed theorem";
   8.116 -      val prop = Pattern.rewrite_term tsg
   8.117 +      val prop = Pattern.rewrite_term (Sign.tsig_of thy')
   8.118          (map (Logic.dest_equals o prop_of) defs) [] (prop_of thm);
   8.119        val vars = vars_of prop;
   8.120        val vars' = filter_out (fn v =>
   8.121          tname_of (body_type (fastype_of v)) mem rtypes) vars;
   8.122 -      val T = etype_of sign vs [] prop;
   8.123 +      val T = etype_of thy' vs [] prop;
   8.124        val (T', thw) = Type.freeze_thaw_type
   8.125          (if T = nullT then nullT else map fastype_of vars' ---> T);
   8.126 -      val t = map_term_types thw (term_of (read_cterm sign (s1, T')));
   8.127 -      val r' = freeze_thaw (condrew sign eqns
   8.128 -        (procs @ [typeof_proc (Sign.defaultS sign) vs, rlz_proc]))
   8.129 +      val t = map_term_types thw (term_of (read_cterm thy' (s1, T')));
   8.130 +      val r' = freeze_thaw (condrew thy' eqns
   8.131 +        (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
   8.132            (Const ("realizes", T --> propT --> propT) $
   8.133              (if T = nullT then t else list_comb (t, vars')) $ prop);
   8.134        val r = foldr forall_intr r' (map (get_var_type r') vars);
   8.135 -      val prf = Reconstruct.reconstruct_proof sign r (rd s2);
   8.136 +      val prf = Reconstruct.reconstruct_proof thy' r (rd s2);
   8.137      in (name, (vs, (t, prf))) end
   8.138    end;
   8.139  
   8.140 @@ -351,15 +348,14 @@
   8.141  fun realizes_of thy vs t prop =
   8.142    let
   8.143      val thy' = add_syntax thy;
   8.144 -    val sign = sign_of thy';
   8.145      val {realizes_eqns, typeof_eqns, defs, types, ...} =
   8.146        ExtractionData.get thy';
   8.147      val procs = List.concat (map (fst o snd) types);
   8.148      val eqns = Net.merge (#net realizes_eqns, #net typeof_eqns, K false);
   8.149 -    val prop' = Pattern.rewrite_term (Sign.tsig_of sign)
   8.150 +    val prop' = Pattern.rewrite_term (Sign.tsig_of thy')
   8.151        (map (Logic.dest_equals o prop_of) defs) [] prop;
   8.152 -  in freeze_thaw (condrew sign eqns
   8.153 -    (procs @ [typeof_proc (Sign.defaultS sign) vs, rlz_proc]))
   8.154 +  in freeze_thaw (condrew thy' eqns
   8.155 +    (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
   8.156        (Const ("realizes", fastype_of t --> propT --> propT) $ t $ prop')
   8.157    end;
   8.158  
   8.159 @@ -403,7 +399,7 @@
   8.160    in
   8.161      ExtractionData.put
   8.162        {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns,
   8.163 -       types = map (apfst (Sign.intern_type (sign_of thy))) tys @ types,
   8.164 +       types = map (apfst (Sign.intern_type thy)) tys @ types,
   8.165         realizers = realizers, defs = defs, expand = expand, prep = prep} thy
   8.166    end;
   8.167  
   8.168 @@ -466,15 +462,14 @@
   8.169  
   8.170  fun extract thms thy =
   8.171    let
   8.172 -    val sg = sign_of (add_syntax thy);
   8.173 -    val tsg = Sign.tsig_of sg;
   8.174 +    val thy' = add_syntax thy;
   8.175      val {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} =
   8.176        ExtractionData.get thy;
   8.177      val procs = List.concat (map (fst o snd) types);
   8.178      val rtypes = map fst types;
   8.179 -    val typroc = typeof_proc (Sign.defaultS sg);
   8.180 -    val prep = getOpt (prep, K I) sg o ProofRewriteRules.elim_defs sg false defs o
   8.181 -      Reconstruct.expand_proof sg (("", NONE) :: map (apsnd SOME) expand);
   8.182 +    val typroc = typeof_proc (Sign.defaultS thy');
   8.183 +    val prep = getOpt (prep, K I) thy' o ProofRewriteRules.elim_defs thy' false defs o
   8.184 +      Reconstruct.expand_proof thy' (("", NONE) :: map (apsnd SOME) expand);
   8.185      val rrews = Net.merge (#net realizes_eqns, #net typeof_eqns, K false);
   8.186  
   8.187      fun find_inst prop Ts ts vs =
   8.188 @@ -485,7 +480,7 @@
   8.189  
   8.190          fun add_args ((Var ((a, i), _), t), (vs', tye)) =
   8.191            if a mem rvs then
   8.192 -            let val T = etype_of sg vs Ts t
   8.193 +            let val T = etype_of thy' vs Ts t
   8.194              in if T = nullT then (vs', tye)
   8.195                 else (a :: vs', (("'" ^ a, i), T) :: tye)
   8.196              end
   8.197 @@ -497,7 +492,7 @@
   8.198      fun find' s = map snd o List.filter (equal s o fst)
   8.199  
   8.200      fun app_rlz_rews Ts vs t = strip_abs (length Ts) (freeze_thaw
   8.201 -      (condrew sg rrews (procs @ [typroc vs, rlz_proc])) (list_abs
   8.202 +      (condrew thy' rrews (procs @ [typroc vs, rlz_proc])) (list_abs
   8.203          (map (pair "x") (rev Ts), t)));
   8.204  
   8.205      fun realizes_null vs prop = app_rlz_rews [] vs
   8.206 @@ -513,7 +508,7 @@
   8.207  
   8.208        | corr d defs vs ts Ts hs (AbsP (s, SOME prop, prf)) (AbsP (_, _, prf')) t =
   8.209            let
   8.210 -            val T = etype_of sg vs Ts prop;
   8.211 +            val T = etype_of thy' vs Ts prop;
   8.212              val u = if T = nullT then 
   8.213                  (case t of SOME u => SOME (incr_boundvars 1 u) | NONE => NONE)
   8.214                else (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE);
   8.215 @@ -537,7 +532,7 @@
   8.216                 else (case t' of SOME (u $ _) => SOME u | _ => NONE));
   8.217              val u = if not (tname_of T mem rtypes) then t else
   8.218                let
   8.219 -                val eT = etype_of sg vs Ts t;
   8.220 +                val eT = etype_of thy' vs Ts t;
   8.221                  val (r, Us') = if eT = nullT then (nullt, Us) else
   8.222                    (Bound (length Us), eT :: Us);
   8.223                  val u = list_comb (incr_boundvars (length Us') t,
   8.224 @@ -551,7 +546,7 @@
   8.225        | corr d defs vs ts Ts hs (prf1 %% prf2) (prf1' %% prf2') t =
   8.226            let
   8.227              val prop = Reconstruct.prop_of' hs prf2';
   8.228 -            val T = etype_of sg vs Ts prop;
   8.229 +            val T = etype_of thy' vs Ts prop;
   8.230              val (defs1, f, u) = if T = nullT then (defs, t, NONE) else
   8.231                (case t of
   8.232                   SOME (f $ u) => (defs, SOME f, SOME u)
   8.233 @@ -569,7 +564,7 @@
   8.234            let
   8.235              val (vs', tye) = find_inst prop Ts ts vs;
   8.236              val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye;
   8.237 -            val T = etype_of sg vs' [] prop;
   8.238 +            val T = etype_of thy' vs' [] prop;
   8.239              val defs' = if T = nullT then defs
   8.240                else fst (extr d defs vs ts Ts hs prf0)
   8.241            in
   8.242 @@ -582,7 +577,7 @@
   8.243                      val _ = msg d ("Building correctness proof for " ^ quote name ^
   8.244                        (if null vs' then ""
   8.245                         else " (relevant variables: " ^ commas_quote vs' ^ ")"));
   8.246 -                    val prf' = prep (Reconstruct.reconstruct_proof sg prop prf);
   8.247 +                    val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf);
   8.248                      val (defs'', corr_prf) =
   8.249                        corr (d + 1) defs' vs' [] [] [] prf' prf' NONE;
   8.250                      val corr_prop = Reconstruct.prop_of corr_prf;
   8.251 @@ -599,7 +594,7 @@
   8.252              | SOME rs => (case find vs' rs of
   8.253                  SOME (_, prf') => (defs', prf_subst_TVars tye' prf')
   8.254                | NONE => error ("corr: no realizer for instance of theorem " ^
   8.255 -                  quote name ^ ":\n" ^ Sign.string_of_term sg (Envir.beta_norm
   8.256 +                  quote name ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
   8.257                      (Reconstruct.prop_of (proof_combt (prf0, ts))))))
   8.258            end
   8.259  
   8.260 @@ -608,12 +603,12 @@
   8.261              val (vs', tye) = find_inst prop Ts ts vs;
   8.262              val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
   8.263            in
   8.264 -            if etype_of sg vs' [] prop = nullT andalso
   8.265 +            if etype_of thy' vs' [] prop = nullT andalso
   8.266                realizes_null vs' prop aconv prop then (defs, prf0)
   8.267              else case find vs' (Symtab.lookup_multi (realizers, s)) of
   8.268                SOME (_, prf) => (defs, prf_subst_TVars tye' prf)
   8.269              | NONE => error ("corr: no realizer for instance of axiom " ^
   8.270 -                quote s ^ ":\n" ^ Sign.string_of_term sg (Envir.beta_norm
   8.271 +                quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
   8.272                    (Reconstruct.prop_of (proof_combt (prf0, ts)))))
   8.273            end
   8.274  
   8.275 @@ -628,7 +623,7 @@
   8.276  
   8.277        | extr d defs vs ts Ts hs (AbsP (s, SOME t, prf)) =
   8.278            let
   8.279 -            val T = etype_of sg vs Ts t;
   8.280 +            val T = etype_of thy' vs Ts t;
   8.281              val (defs', t) = extr d defs vs [] (T :: Ts) (t :: hs)
   8.282                (incr_pboundvars 0 1 prf)
   8.283            in (defs',
   8.284 @@ -646,7 +641,7 @@
   8.285            let
   8.286              val (defs', f) = extr d defs vs [] Ts hs prf1;
   8.287              val prop = Reconstruct.prop_of' hs prf2;
   8.288 -            val T = etype_of sg vs Ts prop
   8.289 +            val T = etype_of thy' vs Ts prop
   8.290            in
   8.291              if T = nullT then (defs', f) else
   8.292                let val (defs'', t) = extr d defs' vs [] Ts hs prf2
   8.293 @@ -665,7 +660,7 @@
   8.294                      val _ = msg d ("Extracting " ^ quote s ^
   8.295                        (if null vs' then ""
   8.296                         else " (relevant variables: " ^ commas_quote vs' ^ ")"));
   8.297 -                    val prf' = prep (Reconstruct.reconstruct_proof sg prop prf);
   8.298 +                    val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf);
   8.299                      val (defs', t) = extr (d + 1) defs vs' [] [] [] prf';
   8.300                      val (defs'', corr_prf) =
   8.301                        corr (d + 1) defs' vs' [] [] [] prf' prf' (SOME t);
   8.302 @@ -708,7 +703,7 @@
   8.303              | SOME rs => (case find vs' rs of
   8.304                  SOME (t, _) => (defs, subst_TVars tye' t)
   8.305                | NONE => error ("extr: no realizer for instance of theorem " ^
   8.306 -                  quote s ^ ":\n" ^ Sign.string_of_term sg (Envir.beta_norm
   8.307 +                  quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
   8.308                      (Reconstruct.prop_of (proof_combt (prf0, ts))))))
   8.309            end
   8.310  
   8.311 @@ -720,7 +715,7 @@
   8.312              case find vs' (Symtab.lookup_multi (realizers, s)) of
   8.313                SOME (t, _) => (defs, subst_TVars tye' t)
   8.314              | NONE => error ("extr: no realizer for instance of axiom " ^
   8.315 -                quote s ^ ":\n" ^ Sign.string_of_term sg (Envir.beta_norm
   8.316 +                quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
   8.317                    (Reconstruct.prop_of (proof_combt (prf0, ts)))))
   8.318            end
   8.319  
   8.320 @@ -731,7 +726,7 @@
   8.321          val {prop, der = (_, prf), sign, ...} = rep_thm thm;
   8.322          val name = Thm.name_of_thm thm;
   8.323          val _ = assert (name <> "") "extraction: unnamed theorem";
   8.324 -        val _ = assert (etype_of sg vs [] prop <> nullT) ("theorem " ^
   8.325 +        val _ = assert (etype_of thy' vs [] prop <> nullT) ("theorem " ^
   8.326            quote name ^ " has no computational content")
   8.327        in (Reconstruct.reconstruct_proof sign prop prf, vs) end;
   8.328  
   8.329 @@ -739,7 +734,7 @@
   8.330        fst (extr 0 defs vs [] [] [] prf)) ([], map prep_thm thms);
   8.331  
   8.332      fun add_def (s, (vs, ((t, u), (prf, _)))) thy =
   8.333 -      (case Sign.const_type (sign_of thy) (extr_name s vs) of
   8.334 +      (case Sign.const_type thy (extr_name s vs) of
   8.335           NONE =>
   8.336             let
   8.337               val corr_prop = Reconstruct.prop_of prf;
   8.338 @@ -798,6 +793,6 @@
   8.339  
   8.340  val _ = OuterSyntax.add_parsers [realizersP, realizabilityP, typeofP, extractP];
   8.341  
   8.342 -val etype_of = etype_of o sign_of o add_syntax;
   8.343 +val etype_of = etype_of o add_syntax;
   8.344  
   8.345  end;
     9.1 --- a/src/Pure/axclass.ML	Fri Jun 17 18:33:42 2005 +0200
     9.2 +++ b/src/Pure/axclass.ML	Fri Jun 17 18:35:27 2005 +0200
     9.3 @@ -119,41 +119,40 @@
     9.4      intro: thm,
     9.5      axioms: thm list};
     9.6  
     9.7 -structure AxclassesArgs =
     9.8 -struct
     9.9 +structure AxclassesData = TheoryDataFun
    9.10 +(struct
    9.11    val name = "Pure/axclasses";
    9.12    type T = axclass_info Symtab.table;
    9.13  
    9.14    val empty = Symtab.empty;
    9.15    val copy = I;
    9.16 -  val prep_ext = I;
    9.17 -  fun merge (tab1, tab2) = Symtab.merge (K true) (tab1, tab2);
    9.18 +  val extend = I;
    9.19 +  fun merge _ = Symtab.merge (K true);
    9.20  
    9.21 -  fun print sg tab =
    9.22 +  fun print thy tab =
    9.23      let
    9.24        fun pretty_class c cs = Pretty.block
    9.25 -        (Pretty.str (Sign.extern_class sg c) :: Pretty.str " <" :: Pretty.brk 1 ::
    9.26 -          Pretty.breaks (map (Pretty.str o Sign.extern_class sg) cs));
    9.27 +        (Pretty.str (Sign.extern_class thy c) :: Pretty.str " <" :: Pretty.brk 1 ::
    9.28 +          Pretty.breaks (map (Pretty.str o Sign.extern_class thy) cs));
    9.29  
    9.30        fun pretty_thms name thms = Pretty.big_list (name ^ ":")
    9.31 -        (map (Display.pretty_thm_sg sg) thms);
    9.32 +        (map (Display.pretty_thm_sg thy) thms);
    9.33  
    9.34        fun pretty_axclass (name, {super_classes, intro, axioms}) = Pretty.block (Pretty.fbreaks
    9.35          [pretty_class name super_classes, pretty_thms introN [intro], pretty_thms axiomsN axioms]);
    9.36      in Pretty.writeln (Pretty.chunks (map pretty_axclass (Symtab.dest tab))) end;
    9.37 -end;
    9.38 +end);
    9.39  
    9.40 -structure AxclassesData = TheoryDataFun(AxclassesArgs);
    9.41  val _ = Context.add_setup [AxclassesData.init];
    9.42  val print_axclasses = AxclassesData.print;
    9.43  
    9.44  
    9.45  (* get and put data *)
    9.46  
    9.47 -fun lookup_axclass_info_sg sg c = Symtab.lookup (AxclassesData.get_sg sg, c);
    9.48 +fun lookup_axclass_info thy c = Symtab.lookup (AxclassesData.get thy, c);
    9.49  
    9.50  fun get_axclass_info thy c =
    9.51 -  (case lookup_axclass_info_sg (Theory.sign_of thy) c of
    9.52 +  (case lookup_axclass_info thy c of
    9.53      NONE => error ("Unknown axclass " ^ quote c)
    9.54    | SOME info => info);
    9.55  
    9.56 @@ -163,10 +162,10 @@
    9.57  
    9.58  (* class_axms *)
    9.59  
    9.60 -fun class_axms sign =
    9.61 -  let val classes = Sign.classes sign in
    9.62 -    map (Thm.class_triv sign) classes @
    9.63 -    List.mapPartial (Option.map #intro o lookup_axclass_info_sg sign) classes
    9.64 +fun class_axms thy =
    9.65 +  let val classes = Sign.classes thy in
    9.66 +    map (Thm.class_triv thy) classes @
    9.67 +    List.mapPartial (Option.map #intro o lookup_axclass_info thy) classes
    9.68    end;
    9.69  
    9.70  
    9.71 @@ -183,17 +182,14 @@
    9.72  
    9.73  fun ext_axclass prep_class prep_axm prep_att (bclass, raw_super_classes) raw_axioms_atts thy =
    9.74    let
    9.75 -    val sign = Theory.sign_of thy;
    9.76 -
    9.77 -    val class = Sign.full_name sign bclass;
    9.78 -    val super_classes = map (prep_class sign) raw_super_classes;
    9.79 -    val axms = map (prep_axm sign o fst) raw_axioms_atts;
    9.80 +    val class = Sign.full_name thy bclass;
    9.81 +    val super_classes = map (prep_class thy) raw_super_classes;
    9.82 +    val axms = map (prep_axm thy o fst) raw_axioms_atts;
    9.83      val atts = map (map (prep_att thy) o snd) raw_axioms_atts;
    9.84  
    9.85      (*declare class*)
    9.86      val class_thy =
    9.87        thy |> Theory.add_classes_i [(bclass, super_classes)];
    9.88 -    val class_sign = Theory.sign_of class_thy;
    9.89  
    9.90      (*prepare abstract axioms*)
    9.91      fun abs_axm ax =
    9.92 @@ -205,9 +201,9 @@
    9.93      fun axm_sort (name, ax) =
    9.94        (case term_tfrees ax of
    9.95          [] => []
    9.96 -      | [(_, S)] => if Sign.subsort class_sign ([class], S) then S else err_bad_axsort name class
    9.97 +      | [(_, S)] => if Sign.subsort class_thy ([class], S) then S else err_bad_axsort name class
    9.98        | _ => err_bad_tfrees name);
    9.99 -    val axS = Sign.certify_sort class_sign (List.concat (map axm_sort axms));
   9.100 +    val axS = Sign.certify_sort class_thy (List.concat (map axm_sort axms));
   9.101  
   9.102      val int_axm = Logic.close_form o map_term_tfrees (K (aT axS));
   9.103      fun inclass c = Logic.mk_inclass (aT axS, c);
   9.104 @@ -268,16 +264,16 @@
   9.105  
   9.106  (* prepare classes and arities *)
   9.107  
   9.108 -fun read_class sg c = Sign.certify_class sg (Sign.intern_class sg c);
   9.109 +fun read_class thy c = Sign.certify_class thy (Sign.intern_class thy c);
   9.110  
   9.111 -fun test_classrel sg cc = (Type.add_classrel (Sign.pp sg) [cc] (Sign.tsig_of sg); cc);
   9.112 -fun cert_classrel sg = test_classrel sg o Library.pairself (Sign.certify_class sg);
   9.113 -fun read_classrel sg = test_classrel sg o Library.pairself (read_class sg);
   9.114 +fun test_classrel thy cc = (Type.add_classrel (Sign.pp thy) [cc] (Sign.tsig_of thy); cc);
   9.115 +fun cert_classrel thy = test_classrel thy o Library.pairself (Sign.certify_class thy);
   9.116 +fun read_classrel thy = test_classrel thy o Library.pairself (read_class thy);
   9.117  
   9.118 -fun test_arity sg ar = (Type.add_arities (Sign.pp sg) [ar] (Sign.tsig_of sg); ar);
   9.119 +fun test_arity thy ar = (Type.add_arities (Sign.pp thy) [ar] (Sign.tsig_of thy); ar);
   9.120  
   9.121 -fun prep_arity prep_tycon prep_sort prep sg (t, Ss, x) =
   9.122 -  test_arity sg (prep_tycon sg t, map (prep_sort sg) Ss, prep sg x);
   9.123 +fun prep_arity prep_tycon prep_sort prep thy (t, Ss, x) =
   9.124 +  test_arity thy (prep_tycon thy t, map (prep_sort thy) Ss, prep thy x);
   9.125  
   9.126  val read_arity = prep_arity Sign.intern_type Sign.read_sort Sign.read_sort;
   9.127  val cert_arity = prep_arity (K I) Sign.certify_sort Sign.certify_sort;
   9.128 @@ -289,22 +285,20 @@
   9.129  
   9.130  fun ext_inst_subclass prep_classrel raw_cc tac thy =
   9.131    let
   9.132 -    val sign = Theory.sign_of thy;
   9.133 -    val (c1, c2) = prep_classrel sign raw_cc;
   9.134 -    val txt = quote (Sign.string_of_classrel sign [c1, c2]);
   9.135 +    val (c1, c2) = prep_classrel thy raw_cc;
   9.136 +    val txt = quote (Sign.string_of_classrel thy [c1, c2]);
   9.137      val _ = message ("Proving class inclusion " ^ txt ^ " ...");
   9.138 -    val th = Tactic.prove sign [] [] (mk_classrel (c1, c2)) (K tac) handle ERROR =>
   9.139 +    val th = Tactic.prove thy [] [] (mk_classrel (c1, c2)) (K tac) handle ERROR =>
   9.140        error ("The error(s) above occurred while trying to prove " ^ txt);
   9.141    in add_classrel_thms [th] thy end;
   9.142  
   9.143  fun ext_inst_arity prep_arity raw_arity tac thy =
   9.144    let
   9.145 -    val sign = Theory.sign_of thy;
   9.146 -    val arity = prep_arity sign raw_arity;
   9.147 -    val txt = quote (Sign.string_of_arity sign arity);
   9.148 +    val arity = prep_arity thy raw_arity;
   9.149 +    val txt = quote (Sign.string_of_arity thy arity);
   9.150      val _ = message ("Proving type arity " ^ txt ^ " ...");
   9.151      val props = (mk_arities arity);
   9.152 -    val ths = Tactic.prove_multi sign [] [] props
   9.153 +    val ths = Tactic.prove_multi thy [] [] props
   9.154          (fn _ => Tactic.smart_conjunction_tac (length props) THEN tac)
   9.155        handle ERROR => error ("The error(s) above occurred while trying to prove " ^ txt);
   9.156    in add_arity_thms ths thy end;
   9.157 @@ -327,7 +321,7 @@
   9.158    theory
   9.159    |> IsarThy.multi_theorem_i Drule.internalK I ProofContext.export_standard
   9.160      ("", [fn (thy, th) => (add_thms [th] thy, th)]) []
   9.161 -    (map (fn t => (("", []), [(t, ([], []))])) (mk_prop (Theory.sign_of theory) inst)) int;
   9.162 +    (map (fn t => (("", []), [(t, ([], []))])) (mk_prop theory inst)) int;
   9.163  
   9.164  in
   9.165  
   9.166 @@ -345,7 +339,7 @@
   9.167  
   9.168  fun intro_classes_tac facts st =
   9.169    (ALLGOALS (Method.insert_tac facts THEN'
   9.170 -      REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.sign_of_thm st))))
   9.171 +      REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.theory_of_thm st))))
   9.172      THEN Tactic.distinct_subgoals_tac) st;
   9.173  
   9.174  fun default_intro_classes_tac [] = intro_classes_tac []
   9.175 @@ -410,41 +404,39 @@
   9.176  
   9.177  local
   9.178  
   9.179 -fun prove mk_prop str_of sign prop thms usr_tac =
   9.180 -  (Tactic.prove sign [] [] (mk_prop prop)
   9.181 +fun prove mk_prop str_of thy prop thms usr_tac =
   9.182 +  (Tactic.prove thy [] [] (mk_prop prop)
   9.183        (K (axclass_tac thms THEN (if_none usr_tac all_tac)))
   9.184      handle ERROR => error ("The error(s) above occurred while trying to prove " ^
   9.185 -     quote (str_of sign prop))) |> Drule.standard;
   9.186 +     quote (str_of thy prop))) |> Drule.standard;
   9.187  
   9.188 -val prove_subclass = prove mk_classrel (fn sg => fn (c1, c2) =>
   9.189 -  Pretty.string_of_classrel (Sign.pp sg) [c1, c2]);
   9.190 +val prove_subclass = prove mk_classrel (fn thy => fn (c1, c2) =>
   9.191 +  Pretty.string_of_classrel (Sign.pp thy) [c1, c2]);
   9.192  
   9.193 -val prove_arity = prove mk_arity (fn sg => fn (t, Ss, c) =>
   9.194 -  Pretty.string_of_arity (Sign.pp sg) (t, Ss, [c]));
   9.195 +val prove_arity = prove mk_arity (fn thy => fn (t, Ss, c) =>
   9.196 +  Pretty.string_of_arity (Sign.pp thy) (t, Ss, [c]));
   9.197  
   9.198  fun witnesses thy names thms =
   9.199 -  PureThy.get_thmss thy (map (rpair NONE) names) @ thms @ List.filter is_def (map snd (axioms_of thy));
   9.200 +  PureThy.get_thmss thy (map (rpair NONE) names) @
   9.201 +  thms @
   9.202 +  List.filter is_def (map snd (axioms_of thy));
   9.203  
   9.204  in
   9.205  
   9.206  fun add_inst_subclass_x raw_c1_c2 names thms usr_tac thy =
   9.207 -  let
   9.208 -    val sign = Theory.sign_of thy;
   9.209 -    val (c1, c2) = read_classrel sign raw_c1_c2;
   9.210 -  in
   9.211 -    message ("Proving class inclusion " ^ quote (Sign.string_of_classrel sign [c1, c2]) ^ " ...");
   9.212 -    thy |> add_classrel_thms [prove_subclass sign (c1, c2) (witnesses thy names thms) usr_tac]
   9.213 +  let val (c1, c2) = read_classrel thy raw_c1_c2 in
   9.214 +    message ("Proving class inclusion " ^ quote (Sign.string_of_classrel thy [c1, c2]) ^ " ...");
   9.215 +    thy |> add_classrel_thms [prove_subclass thy (c1, c2) (witnesses thy names thms) usr_tac]
   9.216    end;
   9.217  
   9.218  fun add_inst_arity_x raw_arity names thms usr_tac thy =
   9.219    let
   9.220 -    val sign = Theory.sign_of thy;
   9.221 -    val (t, Ss, cs) = read_arity sign raw_arity;
   9.222 +    val (t, Ss, cs) = read_arity thy raw_arity;
   9.223      val wthms = witnesses thy names thms;
   9.224      fun prove c =
   9.225       (message ("Proving type arity " ^
   9.226 -        quote (Sign.string_of_arity sign (t, Ss, [c])) ^ " ...");
   9.227 -        prove_arity sign (t, Ss, c) wthms usr_tac);
   9.228 +        quote (Sign.string_of_arity thy (t, Ss, [c])) ^ " ...");
   9.229 +        prove_arity thy (t, Ss, c) wthms usr_tac);
   9.230    in add_arity_thms (map prove cs) thy end;
   9.231  
   9.232  end;
    10.1 --- a/src/Pure/codegen.ML	Fri Jun 17 18:33:42 2005 +0200
    10.2 +++ b/src/Pure/codegen.ML	Fri Jun 17 18:35:27 2005 +0200
    10.3 @@ -38,8 +38,8 @@
    10.4    val invoke_tycodegen: theory -> string -> bool ->
    10.5      (exn option * string) Graph.T * typ -> (exn option * string) Graph.T * Pretty.T
    10.6    val mk_id: string -> string
    10.7 -  val mk_const_id: Sign.sg -> string -> string
    10.8 -  val mk_type_id: Sign.sg -> string -> string
    10.9 +  val mk_const_id: theory -> string -> string
   10.10 +  val mk_type_id: theory -> string -> string
   10.11    val rename_term: term -> term
   10.12    val new_names: term -> string list -> string list
   10.13    val new_name: term -> string -> string
   10.14 @@ -50,8 +50,8 @@
   10.15    val eta_expand: term -> term list -> int -> term
   10.16    val strip_tname: string -> string
   10.17    val mk_type: bool -> typ -> Pretty.T
   10.18 -  val mk_term_of: Sign.sg -> bool -> typ -> Pretty.T
   10.19 -  val mk_gen: Sign.sg -> bool -> string list -> string -> typ -> Pretty.T
   10.20 +  val mk_term_of: theory -> bool -> typ -> Pretty.T
   10.21 +  val mk_gen: theory -> bool -> string list -> string -> typ -> Pretty.T
   10.22    val test_fn: (int -> (string * term) list option) ref
   10.23    val test_term: theory -> int -> int -> term -> (string * term) list option
   10.24    val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
   10.25 @@ -121,14 +121,14 @@
   10.26  fun set_iterations iterations ({size, default_type, ...} : test_params) =
   10.27    {size = size, iterations = iterations, default_type = default_type};
   10.28  
   10.29 -fun set_default_type s sg ({size, iterations, ...} : test_params) =
   10.30 +fun set_default_type s thy ({size, iterations, ...} : test_params) =
   10.31    {size = size, iterations = iterations,
   10.32 -   default_type = SOME (typ_of (read_ctyp sg s))};
   10.33 +   default_type = SOME (typ_of (read_ctyp thy s))};
   10.34  
   10.35  (* data kind 'Pure/codegen' *)
   10.36 - 
   10.37 -structure CodegenArgs =
   10.38 -struct
   10.39 +
   10.40 +structure CodegenData = TheoryDataFun
   10.41 +(struct
   10.42    val name = "Pure/codegen";
   10.43    type T =
   10.44      {codegens : (string * term codegen) list,
   10.45 @@ -143,9 +143,9 @@
   10.46      {codegens = [], tycodegens = [], consts = [], types = [], attrs = [],
   10.47       preprocs = [], test_params = default_test_params};
   10.48    val copy = I;
   10.49 -  val prep_ext = I;
   10.50 +  val extend = I;
   10.51  
   10.52 -  fun merge
   10.53 +  fun merge _
   10.54      ({codegens = codegens1, tycodegens = tycodegens1,
   10.55        consts = consts1, types = types1, attrs = attrs1,
   10.56        preprocs = preprocs1, test_params = test_params1},
   10.57 @@ -160,13 +160,12 @@
   10.58       preprocs = merge_alists' preprocs1 preprocs2,
   10.59       test_params = merge_test_params test_params1 test_params2};
   10.60  
   10.61 -  fun print sg ({codegens, tycodegens, ...} : T) =
   10.62 +  fun print _ ({codegens, tycodegens, ...} : T) =
   10.63      Pretty.writeln (Pretty.chunks
   10.64        [Pretty.strs ("term code generators:" :: map fst codegens),
   10.65         Pretty.strs ("type code generators:" :: map fst tycodegens)]);
   10.66 -end;
   10.67 +end);
   10.68  
   10.69 -structure CodegenData = TheoryDataFun(CodegenArgs);
   10.70  val _ = Context.add_setup [CodegenData.init];
   10.71  val print_codegens = CodegenData.print;
   10.72  
   10.73 @@ -265,18 +264,17 @@
   10.74  
   10.75  fun gen_assoc_consts prep_type xs thy = Library.foldl (fn (thy, (s, tyopt, syn)) =>
   10.76    let
   10.77 -    val sg = sign_of thy;
   10.78      val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} =
   10.79        CodegenData.get thy;
   10.80 -    val cname = Sign.intern_const sg s;
   10.81 +    val cname = Sign.intern_const thy s;
   10.82    in
   10.83 -    (case Sign.const_type sg cname of
   10.84 +    (case Sign.const_type thy cname of
   10.85         SOME T =>
   10.86           let val T' = (case tyopt of
   10.87                  NONE => T
   10.88                | SOME ty =>
   10.89 -                  let val U = prep_type sg ty
   10.90 -                  in if Sign.typ_instance sg (U, T) then U
   10.91 +                  let val U = prep_type thy ty
   10.92 +                  in if Sign.typ_instance thy (U, T) then U
   10.93                      else error ("Illegal type constraint for constant " ^ cname)
   10.94                    end)
   10.95           in (case assoc (consts, (cname, T')) of
   10.96 @@ -291,7 +289,7 @@
   10.97    end) (thy, xs);
   10.98  
   10.99  val assoc_consts_i = gen_assoc_consts (K I);
  10.100 -val assoc_consts = gen_assoc_consts (fn sg => typ_of o read_ctyp sg);
  10.101 +val assoc_consts = gen_assoc_consts (typ_of oo read_ctyp);
  10.102  
  10.103  
  10.104  (**** associate types with target language types ****)
  10.105 @@ -322,7 +320,7 @@
  10.106      ("<" :: "^" :: xs, ">") => (true, implode xs)
  10.107    | ("<" :: xs, ">") => (false, implode xs)
  10.108    | _ => sys_error "dest_sym");
  10.109 -  
  10.110 +
  10.111  fun mk_id s = if s = "" then "" else
  10.112    let
  10.113      fun check_str [] = []
  10.114 @@ -341,12 +339,12 @@
  10.115      if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s'
  10.116    end;
  10.117  
  10.118 -fun mk_const_id sg s =
  10.119 -  let val s' = mk_id (Sign.extern_const sg s)
  10.120 +fun mk_const_id thy s =
  10.121 +  let val s' = mk_id (Sign.extern_const thy s)
  10.122    in if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s' end;
  10.123  
  10.124 -fun mk_type_id sg s =
  10.125 -  let val s' = mk_id (Sign.extern_type sg s)
  10.126 +fun mk_type_id thy s =
  10.127 +  let val s' = mk_id (Sign.extern_type thy s)
  10.128    in if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s' end;
  10.129  
  10.130  fun rename_terms ts =
  10.131 @@ -570,11 +568,10 @@
  10.132  fun gen_generate_code prep_term thy =
  10.133    setmp print_mode [] (Pretty.setmp_margin (!margin) (fn xs =>
  10.134    let
  10.135 -    val sg = sign_of thy;
  10.136      val gr = Graph.new_node ("<Top>", (NONE, "")) Graph.empty;
  10.137      val (gr', ps) = foldl_map (fn (gr, (s, t)) => apsnd (pair s)
  10.138        (invoke_codegen thy "<Top>" false (gr, t)))
  10.139 -        (gr, map (apsnd (prep_term sg)) xs)
  10.140 +        (gr, map (apsnd (prep_term thy)) xs)
  10.141      val code =
  10.142        "structure Generated =\nstruct\n\n" ^
  10.143        output_code gr' ["<Top>"] ^
  10.144 @@ -585,7 +582,7 @@
  10.145  
  10.146  val generate_code_i = gen_generate_code (K I);
  10.147  val generate_code = gen_generate_code
  10.148 -  (fn sg => term_of o read_cterm sg o rpair TypeInfer.logicT);
  10.149 +  (fn thy => term_of o read_cterm thy o rpair TypeInfer.logicT);
  10.150  
  10.151  
  10.152  (**** Reflection ****)
  10.153 @@ -603,22 +600,22 @@
  10.154        [Pretty.str "Type", Pretty.brk 1, Pretty.str ("(\"" ^ s ^ "\","),
  10.155         Pretty.brk 1, pretty_list (map (mk_type false) Ts), Pretty.str ")"]);
  10.156  
  10.157 -fun mk_term_of sg p (TVar ((s, i), _)) = Pretty.str
  10.158 +fun mk_term_of _ p (TVar ((s, i), _)) = Pretty.str
  10.159        (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "F")
  10.160 -  | mk_term_of sg p (TFree (s, _)) = Pretty.str (strip_tname s ^ "F")
  10.161 -  | mk_term_of sg p (Type (s, Ts)) = (if p then parens else I) (Pretty.block
  10.162 -      (separate (Pretty.brk 1) (Pretty.str ("term_of_" ^ mk_type_id sg s) ::
  10.163 -        List.concat (map (fn T => [mk_term_of sg true T, mk_type true T]) Ts))));
  10.164 +  | mk_term_of _ p (TFree (s, _)) = Pretty.str (strip_tname s ^ "F")
  10.165 +  | mk_term_of thy p (Type (s, Ts)) = (if p then parens else I) (Pretty.block
  10.166 +      (separate (Pretty.brk 1) (Pretty.str ("term_of_" ^ mk_type_id thy s) ::
  10.167 +        List.concat (map (fn T => [mk_term_of thy true T, mk_type true T]) Ts))));
  10.168  
  10.169  
  10.170  (**** Test data generators ****)
  10.171  
  10.172 -fun mk_gen sg p xs a (TVar ((s, i), _)) = Pretty.str
  10.173 +fun mk_gen _ p xs a (TVar ((s, i), _)) = Pretty.str
  10.174        (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "G")
  10.175 -  | mk_gen sg p xs a (TFree (s, _)) = Pretty.str (strip_tname s ^ "G")
  10.176 -  | mk_gen sg p xs a (Type (s, Ts)) = (if p then parens else I) (Pretty.block
  10.177 -      (separate (Pretty.brk 1) (Pretty.str ("gen_" ^ mk_type_id sg s ^
  10.178 -        (if s mem xs then "'" else "")) :: map (mk_gen sg true xs a) Ts @
  10.179 +  | mk_gen _ p xs a (TFree (s, _)) = Pretty.str (strip_tname s ^ "G")
  10.180 +  | mk_gen thy p xs a (Type (s, Ts)) = (if p then parens else I) (Pretty.block
  10.181 +      (separate (Pretty.brk 1) (Pretty.str ("gen_" ^ mk_type_id thy s ^
  10.182 +        (if s mem xs then "'" else "")) :: map (mk_gen thy true xs a) Ts @
  10.183          (if s mem xs then [Pretty.str a] else []))));
  10.184  
  10.185  val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE);
  10.186 @@ -629,7 +626,6 @@
  10.187        "Term to be tested contains type variables";
  10.188      val _ = assert (null (term_vars t))
  10.189        "Term to be tested contains schematic variables";
  10.190 -    val sg = sign_of thy;
  10.191      val frees = map dest_Free (term_frees t);
  10.192      val szname = variant (map fst frees) "i";
  10.193      val s = "structure TestTerm =\nstruct\n\n" ^
  10.194 @@ -641,7 +637,7 @@
  10.195            Pretty.blk (0, [Pretty.str "let", Pretty.brk 1,
  10.196              Pretty.blk (0, separate Pretty.fbrk (map (fn (s, T) =>
  10.197                Pretty.block [Pretty.str ("val " ^ mk_id s ^ " ="), Pretty.brk 1,
  10.198 -              mk_gen sg false [] "" T, Pretty.brk 1,
  10.199 +              mk_gen thy false [] "" T, Pretty.brk 1,
  10.200                Pretty.str (szname ^ ";")]) frees)),
  10.201              Pretty.brk 1, Pretty.str "in", Pretty.brk 1,
  10.202              Pretty.block [Pretty.str "if ",
  10.203 @@ -652,7 +648,7 @@
  10.204                  List.concat (separate [Pretty.str ",", Pretty.brk 1]
  10.205                    (map (fn (s, T) => [Pretty.block
  10.206                      [Pretty.str ("(" ^ Library.quote (Symbol.escape s) ^ ","), Pretty.brk 1,
  10.207 -                     mk_app false (mk_term_of sg false T)
  10.208 +                     mk_app false (mk_term_of thy false T)
  10.209                         [Pretty.str (mk_id s)], Pretty.str ")"]]) frees)) @
  10.210                    [Pretty.str "]"])]],
  10.211              Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^
  10.212 @@ -670,12 +666,12 @@
  10.213  
  10.214  fun test_goal ({size, iterations, default_type}, tvinsts) i st =
  10.215    let
  10.216 -    val sg = Toplevel.sign_of st;
  10.217 +    val thy = Toplevel.theory_of st;
  10.218      fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
  10.219        | strip t = t;
  10.220      val (gi, frees) = Logic.goal_params
  10.221        (prop_of (snd (snd (Proof.get_goal (Toplevel.proof_of st))))) i;
  10.222 -    val gi' = ObjectLogic.atomize_term sg (map_term_types
  10.223 +    val gi' = ObjectLogic.atomize_term thy (map_term_types
  10.224        (map_type_tfree (fn p as (s, _) => getOpt (assoc (tvinsts, s),
  10.225          getOpt (default_type,TFree p)))) (subst_bounds (frees, strip gi)));
  10.226    in case test_term (Toplevel.theory_of st) size iterations gi' of
  10.227 @@ -683,7 +679,7 @@
  10.228      | SOME cex => writeln ("Counterexample found:\n" ^
  10.229          Pretty.string_of (Pretty.chunks (map (fn (s, t) =>
  10.230            Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1,
  10.231 -            Sign.pretty_term sg t]) cex)))
  10.232 +            Sign.pretty_term thy t]) cex)))
  10.233    end;
  10.234  
  10.235  
  10.236 @@ -753,8 +749,8 @@
  10.237    P.$$$ "=" |-- getOpt (assoc (params, s), Scan.fail)) >> snd;
  10.238  
  10.239  fun parse_tyinst xs =
  10.240 -  (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn sg =>
  10.241 -    fn (x, ys) => (x, (v, typ_of (read_ctyp sg s)) :: ys))) xs;
  10.242 +  (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>
  10.243 +    fn (x, ys) => (x, (v, typ_of (read_ctyp thy s)) :: ys))) xs;
  10.244  
  10.245  fun app [] x = x
  10.246    | app (f :: fs) x = app fs (f x);
  10.247 @@ -768,7 +764,7 @@
  10.248  val testP =
  10.249    OuterSyntax.command "quickcheck" "try to find counterexample for subgoal" K.diag
  10.250    (Scan.option (P.$$$ "[" |-- P.list1
  10.251 -    (   parse_test_params >> (fn f => fn sg => apfst (f sg))
  10.252 +    (   parse_test_params >> (fn f => fn thy => apfst (f thy))
  10.253       || parse_tyinst) --| P.$$$ "]") -- Scan.optional P.nat 1 >>
  10.254      (fn (ps, g) => Toplevel.keep (fn st =>
  10.255        test_goal (app (getOpt (Option.map
    11.1 --- a/src/Pure/goals.ML	Fri Jun 17 18:33:42 2005 +0200
    11.2 +++ b/src/Pure/goals.ML	Fri Jun 17 18:35:27 2005 +0200
    11.3 @@ -1,6 +1,6 @@
    11.4 -(*  Title: 	Pure/goals.ML
    11.5 +(*  Title:      Pure/goals.ML
    11.6      ID:         $Id$
    11.7 -    Author: 	Lawrence C Paulson and Florian Kammueller, Cambridge University Computer Laboratory
    11.8 +    Author:     Lawrence C Paulson and Florian Kammueller, Cambridge University Computer Laboratory
    11.9      Copyright   1993  University of Cambridge
   11.10  
   11.11  Old-style locales and goal stack package.  The goal stack initially
   11.12 @@ -19,71 +19,71 @@
   11.13    val thms: xstring -> thm list
   11.14    type proof
   11.15    val reset_goals       : unit -> unit
   11.16 -  val atomic_goal	: theory -> string -> thm list
   11.17 -  val atomic_goalw	: theory -> thm list -> string -> thm list
   11.18 -  val Goal		: string -> thm list
   11.19 -  val Goalw		: thm list -> string -> thm list
   11.20 -  val ba		: int -> unit
   11.21 -  val back		: unit -> unit
   11.22 -  val bd		: thm -> int -> unit
   11.23 -  val bds		: thm list -> int -> unit
   11.24 -  val be		: thm -> int -> unit
   11.25 -  val bes		: thm list -> int -> unit
   11.26 -  val br		: thm -> int -> unit
   11.27 -  val brs		: thm list -> int -> unit
   11.28 -  val bw		: thm -> unit
   11.29 -  val bws		: thm list -> unit
   11.30 -  val by		: tactic -> unit
   11.31 -  val byev		: tactic list -> unit
   11.32 -  val chop		: unit -> unit
   11.33 -  val choplev		: int -> unit
   11.34 +  val atomic_goal       : theory -> string -> thm list
   11.35 +  val atomic_goalw      : theory -> thm list -> string -> thm list
   11.36 +  val Goal              : string -> thm list
   11.37 +  val Goalw             : thm list -> string -> thm list
   11.38 +  val ba                : int -> unit
   11.39 +  val back              : unit -> unit
   11.40 +  val bd                : thm -> int -> unit
   11.41 +  val bds               : thm list -> int -> unit
   11.42 +  val be                : thm -> int -> unit
   11.43 +  val bes               : thm list -> int -> unit
   11.44 +  val br                : thm -> int -> unit
   11.45 +  val brs               : thm list -> int -> unit
   11.46 +  val bw                : thm -> unit
   11.47 +  val bws               : thm list -> unit
   11.48 +  val by                : tactic -> unit
   11.49 +  val byev              : tactic list -> unit
   11.50 +  val chop              : unit -> unit
   11.51 +  val choplev           : int -> unit
   11.52    val export_thy        : theory -> thm -> thm
   11.53    val export            : thm -> thm
   11.54 -  val Export		: thm -> thm
   11.55 -  val fa		: unit -> unit
   11.56 -  val fd		: thm -> unit
   11.57 -  val fds		: thm list -> unit
   11.58 -  val fe		: thm -> unit
   11.59 -  val fes		: thm list -> unit
   11.60 -  val filter_goal	: (term*term->bool) -> thm list -> int -> thm list
   11.61 -  val fr		: thm -> unit
   11.62 -  val frs		: thm list -> unit
   11.63 -  val getgoal		: int -> term
   11.64 -  val gethyps		: int -> thm list
   11.65 -  val goal		: theory -> string -> thm list
   11.66 -  val goalw		: theory -> thm list -> string -> thm list
   11.67 -  val goalw_cterm	: thm list -> cterm -> thm list
   11.68 -  val pop_proof		: unit -> thm list
   11.69 -  val pr		: unit -> unit
   11.70 +  val Export            : thm -> thm
   11.71 +  val fa                : unit -> unit
   11.72 +  val fd                : thm -> unit
   11.73 +  val fds               : thm list -> unit
   11.74 +  val fe                : thm -> unit
   11.75 +  val fes               : thm list -> unit
   11.76 +  val filter_goal       : (term*term->bool) -> thm list -> int -> thm list
   11.77 +  val fr                : thm -> unit
   11.78 +  val frs               : thm list -> unit
   11.79 +  val getgoal           : int -> term
   11.80 +  val gethyps           : int -> thm list
   11.81 +  val goal              : theory -> string -> thm list
   11.82 +  val goalw             : theory -> thm list -> string -> thm list
   11.83 +  val goalw_cterm       : thm list -> cterm -> thm list
   11.84 +  val pop_proof         : unit -> thm list
   11.85 +  val pr                : unit -> unit
   11.86    val disable_pr        : unit -> unit
   11.87    val enable_pr         : unit -> unit
   11.88 -  val prlev		: int -> unit
   11.89 -  val prlim		: int -> unit
   11.90 -  val premises		: unit -> thm list
   11.91 -  val prin		: term -> unit
   11.92 -  val printyp		: typ -> unit
   11.93 -  val pprint_term	: term -> pprint_args -> unit
   11.94 -  val pprint_typ	: typ -> pprint_args -> unit
   11.95 -  val print_exn		: exn -> 'a
   11.96 -  val print_sign_exn	: Sign.sg -> exn -> 'a
   11.97 -  val prove_goal	: theory -> string -> (thm list -> tactic list) -> thm
   11.98 +  val prlev             : int -> unit
   11.99 +  val prlim             : int -> unit
  11.100 +  val premises          : unit -> thm list
  11.101 +  val prin              : term -> unit
  11.102 +  val printyp           : typ -> unit
  11.103 +  val pprint_term       : term -> pprint_args -> unit
  11.104 +  val pprint_typ        : typ -> pprint_args -> unit
  11.105 +  val print_exn         : exn -> 'a
  11.106 +  val print_sign_exn    : theory -> exn -> 'a
  11.107 +  val prove_goal        : theory -> string -> (thm list -> tactic list) -> thm
  11.108    val prove_goalw      : theory->thm list->string->(thm list->tactic list)->thm
  11.109 -  val prove_goalw_cterm	: thm list->cterm->(thm list->tactic list)->thm
  11.110 -  val prove_goalw_cterm_nocheck	: thm list->cterm->(thm list->tactic list)->thm
  11.111 +  val prove_goalw_cterm : thm list->cterm->(thm list->tactic list)->thm
  11.112 +  val prove_goalw_cterm_nocheck : thm list->cterm->(thm list->tactic list)->thm
  11.113    val quick_and_dirty_prove_goalw_cterm: theory -> thm list -> cterm
  11.114      -> (thm list -> tactic list) -> thm
  11.115    val simple_prove_goal_cterm : cterm->(thm list->tactic list)->thm
  11.116 -  val push_proof	: unit -> unit
  11.117 -  val read		: string -> term
  11.118 -  val ren		: string -> int -> unit
  11.119 -  val restore_proof	: proof -> thm list
  11.120 -  val result		: unit -> thm  
  11.121 +  val push_proof        : unit -> unit
  11.122 +  val read              : string -> term
  11.123 +  val ren               : string -> int -> unit
  11.124 +  val restore_proof     : proof -> thm list
  11.125 +  val result            : unit -> thm
  11.126    val result_error_fn   : (thm -> string -> thm) ref
  11.127 -  val rotate_proof	: unit -> thm list
  11.128 -  val uresult		: unit -> thm  
  11.129 -  val save_proof	: unit -> proof
  11.130 -  val topthm		: unit -> thm
  11.131 -  val undo		: unit -> unit
  11.132 +  val rotate_proof      : unit -> thm list
  11.133 +  val uresult           : unit -> thm
  11.134 +  val save_proof        : unit -> proof
  11.135 +  val topthm            : unit -> thm
  11.136 +  val undo              : unit -> unit
  11.137    val bind_thm          : string * thm -> unit
  11.138    val bind_thms         : string * thm list -> unit
  11.139    val qed               : string -> unit
  11.140 @@ -112,7 +112,7 @@
  11.141    val open_locale: xstring -> theory -> theory
  11.142    val close_locale: xstring -> theory -> theory
  11.143    val print_scope: theory -> unit
  11.144 -  val read_cterm: Sign.sg -> string * typ -> cterm
  11.145 +  val read_cterm: theory -> string * typ -> cterm
  11.146  end;
  11.147  
  11.148  structure Goals: GOALS =
  11.149 @@ -125,11 +125,11 @@
  11.150  
  11.151      locale Locale_name =
  11.152        fixes   (*variables that are fixed in the locale's scope*)
  11.153 -	v :: T
  11.154 +        v :: T
  11.155        assumes (*meta-hypothesis that hold in the locale*)
  11.156 -	Asm_name "meta-formula"  
  11.157 +        Asm_name "meta-formula"
  11.158        defines (*local definitions of fixed variables in terms of others*)
  11.159 -	v_def "v x == ...x..."
  11.160 +        v_def "v x == ...x..."
  11.161  *)
  11.162  
  11.163  (** type locale **)
  11.164 @@ -144,13 +144,13 @@
  11.165    defaults: (string * sort) list * (string * typ) list * string list};
  11.166  
  11.167  fun make_locale ancestor consts nosyn rules defs thms defaults =
  11.168 -  {ancestor = ancestor, consts = consts, nosyn = nosyn, rules = rules, 
  11.169 +  {ancestor = ancestor, consts = consts, nosyn = nosyn, rules = rules,
  11.170     defs = defs, thms = thms, defaults = defaults}: locale;
  11.171  
  11.172 -fun pretty_locale sg (name, {ancestor, consts, rules, defs, nosyn = _, thms = _, defaults = _}) =
  11.173 +fun pretty_locale thy (name, {ancestor, consts, rules, defs, nosyn = _, thms = _, defaults = _}) =
  11.174    let
  11.175 -    val prt_typ = Pretty.quote o Sign.pretty_typ sg;
  11.176 -    val prt_term = Pretty.quote o Sign.pretty_term sg;
  11.177 +    val prt_typ = Pretty.quote o Sign.pretty_typ thy;
  11.178 +    val prt_term = Pretty.quote o Sign.pretty_term thy;
  11.179  
  11.180      fun pretty_const (c, T) = Pretty.block
  11.181        [Pretty.str (c ^ " ::"), Pretty.brk 1, prt_typ T];
  11.182 @@ -182,48 +182,43 @@
  11.183  fun make_locale_data space locales scope =
  11.184    {space = space, locales = locales, scope = scope}: locale_data;
  11.185  
  11.186 -structure LocalesArgs =
  11.187 -struct
  11.188 +structure LocalesData = TheoryDataFun
  11.189 +(struct
  11.190    val name = "Pure/old-locales";
  11.191    type T = locale_data;
  11.192  
  11.193    val empty = make_locale_data NameSpace.empty Symtab.empty (ref []);
  11.194    fun copy {space, locales, scope = ref locs} = make_locale_data space locales (ref locs);
  11.195 -  fun prep_ext {space, locales, scope = _} = make_locale_data space locales (ref []);
  11.196 -  fun merge ({space = space1, locales = locales1, scope = _},
  11.197 +  fun extend {space, locales, scope = _} = make_locale_data space locales (ref []);
  11.198 +  fun merge _ ({space = space1, locales = locales1, scope = _},
  11.199      {space = space2, locales = locales2, scope = _}) =
  11.200        make_locale_data (NameSpace.merge (space1, space2))
  11.201          (Symtab.merge (K true) (locales1, locales2))
  11.202          (ref []);
  11.203  
  11.204 -  fun print sg {space, locales, scope} =
  11.205 +  fun print thy {space, locales, scope} =
  11.206      let
  11.207        val locs = NameSpace.extern_table (space, locales);
  11.208        val scope_names = rev (map (NameSpace.extern space o fst) (! scope));
  11.209      in
  11.210 -      [Display.pretty_name_space ("locale name space", space),
  11.211 -        Pretty.big_list "locales:" (map (pretty_locale sg) locs),
  11.212 +      [Pretty.big_list "locales:" (map (pretty_locale thy) locs),
  11.213          Pretty.strs ("current scope:" :: scope_names)]
  11.214        |> Pretty.chunks |> Pretty.writeln
  11.215      end;
  11.216 -end;
  11.217 +end);
  11.218  
  11.219 -
  11.220 -structure LocalesData = TheoryDataFun(LocalesArgs);
  11.221  val _ = Context.add_setup [LocalesData.init];
  11.222  val print_locales = LocalesData.print;
  11.223  
  11.224  
  11.225  (* access locales *)
  11.226  
  11.227 -fun get_locale_sg sg name = Symtab.lookup (#locales (LocalesData.get_sg sg), name);
  11.228 -
  11.229 -val get_locale = get_locale_sg o Theory.sign_of;
  11.230 +fun get_locale thy name = Symtab.lookup (#locales (LocalesData.get thy), name);
  11.231  
  11.232  fun put_locale (name, locale) thy =
  11.233    let
  11.234      val {space, locales, scope} = LocalesData.get thy;
  11.235 -    val space' = Sign.declare_name (Theory.sign_of thy) name space;
  11.236 +    val space' = Sign.declare_name thy name space;
  11.237      val locales' = Symtab.update ((name, locale), locales);
  11.238    in thy |> LocalesData.put (make_locale_data space' locales' scope) end;
  11.239  
  11.240 @@ -236,11 +231,9 @@
  11.241  
  11.242  (* access scope *)
  11.243  
  11.244 -fun get_scope_sg sg =
  11.245 -  if Sign.eq_sg (sg, Theory.sign_of ProtoPure.thy) then []
  11.246 -  else ! (#scope (LocalesData.get_sg sg));
  11.247 -
  11.248 -val get_scope = get_scope_sg o Theory.sign_of;
  11.249 +fun get_scope thy =
  11.250 +  if eq_thy (thy, ProtoPure.thy) then []
  11.251 +  else ! (#scope (LocalesData.get thy));
  11.252  
  11.253  fun change_scope f thy =
  11.254    let val {scope, ...} = LocalesData.get thy
  11.255 @@ -264,26 +257,26 @@
  11.256        fun opn lc th = (change_scope (cons lc) th; th)
  11.257    in case anc of
  11.258           NONE => opn loc thy
  11.259 -       | SOME(loc') => 
  11.260 -           if loc' mem (map fst cur_sc) 
  11.261 +       | SOME(loc') =>
  11.262 +           if loc' mem (map fst cur_sc)
  11.263             then opn loc thy
  11.264 -           else (warning ("Opening locale " ^ quote loc' ^ ", required by " ^ 
  11.265 -			  quote xname);
  11.266 +           else (warning ("Opening locale " ^ quote loc' ^ ", required by " ^
  11.267 +                          quote xname);
  11.268                   opn loc (open_locale (Sign.base_name loc') thy))
  11.269    end;
  11.270  
  11.271  fun pop_locale [] = error "Currently no open locales"
  11.272    | pop_locale (_ :: locs) = locs;
  11.273  
  11.274 -fun close_locale name thy = 
  11.275 +fun close_locale name thy =
  11.276     let val lname = (case get_scope thy of (ln,_)::_ => ln
  11.277                                          | _ => error "No locales are open!")
  11.278 -       val ok = (name = Sign.base_name lname) handle _ => false
  11.279 +       val ok = name = Sign.base_name lname
  11.280     in if ok then (change_scope pop_locale thy; thy)
  11.281        else error ("locale " ^ name ^ " is not top of scope; top is " ^ lname)
  11.282     end;
  11.283  
  11.284 -fun print_scope thy = 
  11.285 +fun print_scope thy =
  11.286  Pretty.writeln (Pretty.strs ("current scope:" :: rev(map (Sign.base_name o fst) (get_scope thy))));
  11.287  
  11.288  (*implicit context versions*)
  11.289 @@ -295,11 +288,10 @@
  11.290  (** functions for goals.ML **)
  11.291  
  11.292  (* in_locale: check if hyps (: term list) of a proof are contained in the
  11.293 -   (current) scope. This function is needed in prepare_proof. It needs to
  11.294 -   refer to the signature, because theory is not available in prepare_proof. *)
  11.295 +   (current) scope. This function is needed in prepare_proof. *)
  11.296  
  11.297 -fun in_locale hyps sg =
  11.298 -    let val cur_sc = get_scope_sg sg;
  11.299 +fun in_locale hyps thy =
  11.300 +    let val cur_sc = get_scope thy;
  11.301          val rule_lists = map (#rules o snd) cur_sc;
  11.302          val def_lists = map (#defs o snd) cur_sc;
  11.303          val rules = map snd (foldr (op union) [] rule_lists);
  11.304 @@ -311,12 +303,10 @@
  11.305  
  11.306  
  11.307  (* is_open_loc: check if any locale is open, i.e. in the scope of the current thy *)
  11.308 -fun is_open_loc_sg sign =
  11.309 -    let val cur_sc = get_scope_sg sign
  11.310 +fun is_open_loc thy =
  11.311 +    let val cur_sc = get_scope thy
  11.312      in not(null(cur_sc)) end;
  11.313  
  11.314 -val is_open_loc = is_open_loc_sg o Theory.sign_of;
  11.315 -
  11.316  
  11.317  (* get theorems *)
  11.318  
  11.319 @@ -336,7 +326,7 @@
  11.320  
  11.321  (* get the defaults of a locale, for extension *)
  11.322  
  11.323 -fun get_defaults thy name = 
  11.324 +fun get_defaults thy name =
  11.325    let val (lname, loc) = the_locale thy name;
  11.326    in #defaults(loc)
  11.327    end;
  11.328 @@ -346,15 +336,15 @@
  11.329  
  11.330  (* prepare types *)
  11.331  
  11.332 -fun read_typ sg (envT, s) =
  11.333 +fun read_typ thy (envT, s) =
  11.334    let
  11.335      fun def_sort (x, ~1) = assoc (envT, x)
  11.336        | def_sort _ = NONE;
  11.337 -    val T = Type.no_tvars (Sign.read_typ (sg, def_sort) s) handle TYPE (msg, _, _) => error msg;
  11.338 +    val T = Type.no_tvars (Sign.read_typ (thy, def_sort) s) handle TYPE (msg, _, _) => error msg;
  11.339    in (Term.add_typ_tfrees (T, envT), T) end;
  11.340  
  11.341 -fun cert_typ sg (envT, raw_T) =
  11.342 -  let val T = Type.no_tvars (Sign.certify_typ sg raw_T) handle TYPE (msg, _, _) => error msg
  11.343 +fun cert_typ thy (envT, raw_T) =
  11.344 +  let val T = Type.no_tvars (Sign.certify_typ thy raw_T) handle TYPE (msg, _, _) => error msg
  11.345    in (Term.add_typ_tfrees (T, envT), T) end;
  11.346  
  11.347  
  11.348 @@ -365,20 +355,20 @@
  11.349  fun enter_term t (envS, envT, used) =
  11.350    (Term.add_term_tfrees (t, envS), add_frees (envT, t), Term.add_term_tfree_names (t, used));
  11.351  
  11.352 -fun read_axm sg ((envS, envT, used), (name, s)) =
  11.353 +fun read_axm thy ((envS, envT, used), (name, s)) =
  11.354    let
  11.355      fun def_sort (x, ~1) = assoc (envS, x)
  11.356        | def_sort _ = NONE;
  11.357      fun def_type (x, ~1) = assoc (envT, x)
  11.358        | def_type _ = NONE;
  11.359 -    val (_, t) = Theory.read_def_axm (sg, def_type, def_sort) used (name, s);
  11.360 +    val (_, t) = Theory.read_def_axm (thy, def_type, def_sort) used (name, s);
  11.361    in
  11.362      (enter_term t (envS, envT, used), t)
  11.363    end;
  11.364  
  11.365  
  11.366 -fun cert_axm sg ((envS, envT, used), (name, raw_t)) =
  11.367 -  let val (_, t) = Theory.cert_axm sg (name, raw_t)
  11.368 +fun cert_axm thy ((envS, envT, used), (name, raw_t)) =
  11.369 +  let val (_, t) = Theory.cert_axm thy (name, raw_t)
  11.370    in (enter_term t (envS, envT, used), t) end;
  11.371  
  11.372  
  11.373 @@ -386,8 +376,8 @@
  11.374     that already exist for subterms. If no locale is open, this function is equal to
  11.375     Thm.read_cterm  *)
  11.376  
  11.377 -fun read_cterm sign =
  11.378 -    let val cur_sc = get_scope_sg sign;
  11.379 +fun read_cterm thy =
  11.380 +    let val cur_sc = get_scope thy;
  11.381          val defaults = map (#defaults o snd) cur_sc;
  11.382          val envS = List.concat (map #1 defaults);
  11.383          val envT = List.concat (map #2 defaults);
  11.384 @@ -396,15 +386,15 @@
  11.385            | def_sort _ = NONE;
  11.386          fun def_type (x, ~1) = assoc (envT, x)
  11.387            | def_type _ = NONE;
  11.388 -    in (if (is_open_loc_sg sign)
  11.389 -        then (#1 o read_def_cterm (sign, def_type, def_sort) used true)
  11.390 -        else Thm.read_cterm sign)
  11.391 +    in (if (is_open_loc thy)
  11.392 +        then (#1 o read_def_cterm (thy, def_type, def_sort) used true)
  11.393 +        else Thm.read_cterm thy)
  11.394      end;
  11.395  
  11.396  (* basic functions needed for definitions and display *)
  11.397  (* collect all locale constants of a scope, i.e. a list of locales *)
  11.398 -fun collect_consts sg =
  11.399 -    let val cur_sc = get_scope_sg sg;
  11.400 +fun collect_consts thy =
  11.401 +    let val cur_sc = get_scope thy;
  11.402          val locale_list = map snd cur_sc;
  11.403          val const_list = List.concat (map #consts locale_list)
  11.404      in map fst const_list end;
  11.405 @@ -447,7 +437,7 @@
  11.406  
  11.407  (* assume a definition, i.e assume the cterm of a definiton term and then eliminate
  11.408     the binding !!, so that the def can be applied as rewrite. The meta hyp will still contain !! *)
  11.409 -fun prep_hyps clist sg = forall_elim_vars(0) o Thm.assume o (Thm.cterm_of sg);
  11.410 +fun prep_hyps clist thy = forall_elim_vars(0) o Thm.assume o (Thm.cterm_of thy);
  11.411  
  11.412  
  11.413  (* concrete syntax *)
  11.414 @@ -460,21 +450,20 @@
  11.415  (* add_locale *)
  11.416  
  11.417  fun gen_add_locale prep_typ prep_term bname bancestor raw_consts raw_rules raw_defs thy =
  11.418 -  let val sign = Theory.sign_of thy;
  11.419 +  let
  11.420 +    val name = Sign.full_name thy bname;
  11.421  
  11.422 -    val name = Sign.full_name sign bname;
  11.423 -
  11.424 -    val (envSb, old_loc_consts, _) = 
  11.425 +    val (envSb, old_loc_consts, _) =
  11.426                      case bancestor of
  11.427                         SOME(loc) => (get_defaults thy loc)
  11.428                       | NONE      => ([],[],[]);
  11.429  
  11.430 -    val old_nosyn = case bancestor of 
  11.431 +    val old_nosyn = case bancestor of
  11.432                         SOME(loc) => #nosyn(#2(the_locale thy loc))
  11.433                       | NONE      => [];
  11.434  
  11.435      (* Get the full name of the ancestor *)
  11.436 -    val ancestor = case bancestor of 
  11.437 +    val ancestor = case bancestor of
  11.438                         SOME(loc) => SOME(#1(the_locale thy loc))
  11.439                       | NONE      => NONE;
  11.440  
  11.441 @@ -485,7 +474,7 @@
  11.442          val c = Syntax.const_name raw_c raw_mx;
  11.443          val c_syn = mark_syn c;
  11.444          val mx = Syntax.fix_mixfix raw_c raw_mx;
  11.445 -        val (envS', T) = prep_typ sign (envS, raw_T) handle ERROR =>
  11.446 +        val (envS', T) = prep_typ thy (envS, raw_T) handle ERROR =>
  11.447            error ("The error(s) above occured in locale constant " ^ quote c);
  11.448          val trfun = if mx = Syntax.NoSyn then NONE else SOME (c_syn, mk_loc_tr c);
  11.449        in (envS', ((c, T), (c_syn, T, mx), trfun)) end;
  11.450 @@ -505,38 +494,36 @@
  11.451        |> Theory.add_modesyntax_i Syntax.default_mode loc_syn
  11.452        |> Theory.add_trfuns ([], loc_trfuns, [], []);
  11.453  
  11.454 -    val syntax_sign = Theory.sign_of syntax_thy;
  11.455 -
  11.456  
  11.457      (* prepare rules and defs *)
  11.458  
  11.459      fun prep_axiom (env, (a, raw_t)) =
  11.460        let
  11.461 -        val (env', t) = prep_term syntax_sign (env, (a, raw_t)) handle ERROR =>
  11.462 +        val (env', t) = prep_term syntax_thy (env, (a, raw_t)) handle ERROR =>
  11.463            error ("The error(s) above occured in locale rule / definition " ^ quote a);
  11.464        in (env', (a, t)) end;
  11.465  
  11.466      val ((envS1, envT1, used1), loc_rules) =
  11.467        foldl_map prep_axiom ((envS0, loc_consts, map fst envS0), raw_rules);
  11.468 -    val (defaults, loc_defs) = 
  11.469 -	foldl_map prep_axiom ((envS1, envT1, used1), raw_defs);
  11.470 +    val (defaults, loc_defs) =
  11.471 +        foldl_map prep_axiom ((envS1, envT1, used1), raw_defs);
  11.472  
  11.473 -    val old_loc_consts = collect_consts syntax_sign;
  11.474 +    val old_loc_consts = collect_consts syntax_thy;
  11.475      val new_loc_consts = (map #1 loc_consts);
  11.476      val all_loc_consts = old_loc_consts @ new_loc_consts;
  11.477  
  11.478 -    val (defaults, loc_defs_terms) = 
  11.479 -	foldl_map (abs_over_free all_loc_consts) (defaults, loc_defs);
  11.480 -    val loc_defs_thms = 
  11.481 -	map (apsnd (prep_hyps (map #1 loc_consts) syntax_sign)) loc_defs_terms;
  11.482 -    val (defaults, loc_thms_terms) = 
  11.483 -	foldl_map (abs_over_free all_loc_consts) (defaults, loc_rules);
  11.484 -    val loc_thms = map (apsnd (prep_hyps (map #1 loc_consts) syntax_sign))
  11.485 -		       (loc_thms_terms)
  11.486 +    val (defaults, loc_defs_terms) =
  11.487 +        foldl_map (abs_over_free all_loc_consts) (defaults, loc_defs);
  11.488 +    val loc_defs_thms =
  11.489 +        map (apsnd (prep_hyps (map #1 loc_consts) syntax_thy)) loc_defs_terms;
  11.490 +    val (defaults, loc_thms_terms) =
  11.491 +        foldl_map (abs_over_free all_loc_consts) (defaults, loc_rules);
  11.492 +    val loc_thms = map (apsnd (prep_hyps (map #1 loc_consts) syntax_thy))
  11.493 +                       (loc_thms_terms)
  11.494                     @ loc_defs_thms;
  11.495  
  11.496  
  11.497 -    (* error messages *) 
  11.498 +    (* error messages *)
  11.499  
  11.500      fun locale_error msg = error (msg ^ "\nFor locale " ^ quote name);
  11.501  
  11.502 @@ -544,31 +531,31 @@
  11.503        if is_none (get_locale thy name) then []
  11.504        else ["Duplicate definition of locale " ^ quote name];
  11.505  
  11.506 -    (* check if definientes are locale constants 
  11.507 +    (* check if definientes are locale constants
  11.508         (in the same locale, so no redefining!) *)
  11.509      val err_def_head =
  11.510 -      let fun peal_appl t = 
  11.511 -            case t of 
  11.512 +      let fun peal_appl t =
  11.513 +            case t of
  11.514                   t1 $ t2 => peal_appl t1
  11.515                 | Free(t) => t
  11.516                 | _ => locale_error ("Bad form of LHS in locale definition");
  11.517 -	  fun lhs (_, Const ("==" , _) $  d1 $ d2) = peal_appl d1
  11.518 -	    | lhs _ = locale_error ("Definitions must use the == relation");
  11.519 +          fun lhs (_, Const ("==" , _) $  d1 $ d2) = peal_appl d1
  11.520 +            | lhs _ = locale_error ("Definitions must use the == relation");
  11.521            val defs = map lhs loc_defs;
  11.522            val check = defs subset loc_consts
  11.523 -      in if check then [] 
  11.524 +      in if check then []
  11.525           else ["defined item not declared fixed in locale " ^ quote name]
  11.526 -      end; 
  11.527 +      end;
  11.528  
  11.529      (* check that variables on rhs of definitions are either fixed or on lhs *)
  11.530 -    val err_var_rhs = 
  11.531 -      let fun compare_var_sides (t, (_, Const ("==", _) $ d1 $ d2)) = 
  11.532 -		let val varl1 = difflist d1 all_loc_consts;
  11.533 -		    val varl2 = difflist d2 all_loc_consts
  11.534 -		in t andalso (varl2 subset varl1)
  11.535 -		end
  11.536 -            | compare_var_sides (_,_) = 
  11.537 -		locale_error ("Definitions must use the == relation")
  11.538 +    val err_var_rhs =
  11.539 +      let fun compare_var_sides (t, (_, Const ("==", _) $ d1 $ d2)) =
  11.540 +                let val varl1 = difflist d1 all_loc_consts;
  11.541 +                    val varl2 = difflist d2 all_loc_consts
  11.542 +                in t andalso (varl2 subset varl1)
  11.543 +                end
  11.544 +            | compare_var_sides (_,_) =
  11.545 +                locale_error ("Definitions must use the == relation")
  11.546            val check = Library.foldl compare_var_sides (true, loc_defs)
  11.547        in if check then []
  11.548           else ["nonfixed variable on right hand side of a locale definition in locale " ^ quote name]
  11.549 @@ -580,8 +567,8 @@
  11.550      else error (cat_lines errs);
  11.551  
  11.552      syntax_thy
  11.553 -    |> put_locale (name, 
  11.554 -		   make_locale ancestor loc_consts nosyn loc_thms_terms 
  11.555 +    |> put_locale (name,
  11.556 +                   make_locale ancestor loc_consts nosyn loc_thms_terms
  11.557                                          loc_defs_terms   loc_thms defaults)
  11.558    end;
  11.559  
  11.560 @@ -612,14 +599,14 @@
  11.561    | const_ssubst_list (s :: l) t = const_ssubst_list l (const_ssubst t s);
  11.562  
  11.563  (* pretty_term *)
  11.564 -fun pretty_term sign =
  11.565 -    if (is_open_loc_sg sign) then
  11.566 -        let val locale_list = map snd(get_scope_sg sign);
  11.567 +fun pretty_term thy =
  11.568 +    if (is_open_loc thy) then
  11.569 +        let val locale_list = map snd(get_scope thy);
  11.570              val nosyn = List.concat (map #nosyn locale_list);
  11.571 -            val str_list = (collect_consts sign) \\ nosyn
  11.572 -        in Sign.pretty_term sign o (const_ssubst_list str_list)
  11.573 +            val str_list = (collect_consts thy) \\ nosyn
  11.574 +        in Sign.pretty_term thy o (const_ssubst_list str_list)
  11.575          end
  11.576 -    else Sign.pretty_term sign;
  11.577 +    else Sign.pretty_term thy;
  11.578  
  11.579  
  11.580  
  11.581 @@ -644,10 +631,9 @@
  11.582  fun init_mkresult _ = error "No goal has been supplied in subgoal module";
  11.583  val curr_mkresult = ref (init_mkresult: bool*thm->thm);
  11.584  
  11.585 -val dummy = trivial(read_cterm (Theory.sign_of ProtoPure.thy)
  11.586 -    ("PROP No_goal_has_been_supplied",propT));
  11.587 +val dummy = Thm.trivial (read_cterm ProtoPure.thy ("PROP No_goal_has_been_supplied", propT));
  11.588  
  11.589 -(*List of previous goal stacks, for the undo operation.  Set by setstate. 
  11.590 +(*List of previous goal stacks, for the undo operation.  Set by setstate.
  11.591    A list of lists!*)
  11.592  val undo_list = ref([[(dummy, Seq.empty)]] : gstack list);
  11.593  
  11.594 @@ -662,9 +648,9 @@
  11.595  
  11.596  (*** Setting up goal-directed proof ***)
  11.597  
  11.598 -(*Generates the list of new theories when the proof state's signature changes*)
  11.599 -fun sign_error (sign,sign') =
  11.600 -  let val names = Sign.stamp_names_of sign' \\ Sign.stamp_names_of sign
  11.601 +(*Generates the list of new theories when the proof state's theory changes*)
  11.602 +fun thy_error (thy,thy') =
  11.603 +  let val names = Context.names_of thy' \\ Context.names_of thy
  11.604    in  case names of
  11.605          [name] => "\nNew theory: " ^ name
  11.606        | _       => "\nNew theories: " ^ space_implode ", " names
  11.607 @@ -689,23 +675,22 @@
  11.608    end;
  11.609  
  11.610  (** exporting a theorem out of a locale means turning all meta-hyps into assumptions
  11.611 -    and expand and cancel the locale definitions. 
  11.612 +    and expand and cancel the locale definitions.
  11.613      export goes through all levels in case of nested locales, whereas
  11.614      export_thy just goes one up. **)
  11.615  
  11.616 -fun get_top_scope_thms thy = 
  11.617 -   let val sc = (get_scope_sg (Theory.sign_of thy))
  11.618 -   in if (null sc) then (warning "No locale in theory"; [])
  11.619 +fun get_top_scope_thms thy =
  11.620 +   let val sc = get_scope thy
  11.621 +   in if null sc then (warning "No locale in theory"; [])
  11.622        else map Thm.prop_of (map #2 (#thms(snd(hd sc))))
  11.623     end;
  11.624  
  11.625 -fun implies_intr_some_hyps thy A_set th = 
  11.626 -   let 
  11.627 -       val sign = Theory.sign_of thy;
  11.628 +fun implies_intr_some_hyps thy A_set th =
  11.629 +   let
  11.630         val used_As = A_set inter #hyps(rep_thm(th));
  11.631 -       val ctl = map (cterm_of sign) used_As
  11.632 +       val ctl = map (cterm_of thy) used_As
  11.633     in Library.foldl (fn (x, y) => Thm.implies_intr y x) (th, ctl)
  11.634 -   end; 
  11.635 +   end;
  11.636  
  11.637  fun standard_some thy A_set th =
  11.638    let val {maxidx,...} = rep_thm th
  11.639 @@ -716,7 +701,7 @@
  11.640         |> zero_var_indexes |> Thm.varifyT |> Thm.compress
  11.641    end;
  11.642  
  11.643 -fun export_thy thy th = 
  11.644 +fun export_thy thy th =
  11.645    let val A_set = get_top_scope_thms thy
  11.646    in
  11.647       standard_some thy [] (Seq.hd ((REPEAT (FIRSTGOAL (rtac reflexive_thm))) (standard_some thy A_set th)))
  11.648 @@ -733,107 +718,106 @@
  11.649    "Goal::prop=>prop" to avoid assumptions being returned separately.
  11.650  *)
  11.651  fun prepare_proof atomic rths chorn =
  11.652 -  let val {sign, t=horn,...} = rep_cterm chorn;
  11.653 +  let val {thy, t=horn,...} = rep_cterm chorn;
  11.654        val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg;
  11.655        val (As, B) = Logic.strip_horn horn;
  11.656        val atoms = atomic andalso
  11.657              forall (fn t => not(Logic.is_implies t orelse Logic.is_all t)) As;
  11.658        val (As,B) = if atoms then ([],horn) else (As,B);
  11.659 -      val cAs = map (cterm_of sign) As;
  11.660 +      val cAs = map (cterm_of thy) As;
  11.661        val prems = map (rewrite_rule rths o forall_elim_vars 0 o Thm.assume) cAs;
  11.662 -      val cB = cterm_of sign B;
  11.663 +      val cB = cterm_of thy B;
  11.664        val st0 = let val st = Drule.impose_hyps cAs (Drule.mk_triv_goal cB)
  11.665                  in  rewrite_goals_rule rths st end
  11.666        (*discharges assumptions from state in the order they appear in goal;
  11.667 -	checks (if requested) that resulting theorem is equivalent to goal. *)
  11.668 +        checks (if requested) that resulting theorem is equivalent to goal. *)
  11.669        fun mkresult (check,state) =
  11.670          let val state = Seq.hd (flexflex_rule state)
  11.671 -	    		handle THM _ => state   (*smash flexflex pairs*)
  11.672 -	    val ngoals = nprems_of state
  11.673 +                        handle THM _ => state   (*smash flexflex pairs*)
  11.674 +            val ngoals = nprems_of state
  11.675              val ath = implies_intr_list cAs state
  11.676              val th = ath RS Drule.rev_triv_goal
  11.677 -            val {hyps,prop,sign=sign',...} = rep_thm th
  11.678 +            val {hyps,prop,thy=thy',...} = rep_thm th
  11.679              val final_th = if (null(hyps)) then standard th else varify th
  11.680          in  if not check then final_th
  11.681 -	    else if not (Sign.eq_sg(sign,sign')) then !result_error_fn state
  11.682 -		("Signature of proof state has changed!" ^
  11.683 -		 sign_error (sign,sign'))
  11.684 +            else if not (eq_thy(thy,thy')) then !result_error_fn state
  11.685 +                ("Theory of proof state has changed!" ^
  11.686 +                 thy_error (thy,thy'))
  11.687              else if ngoals>0 then !result_error_fn state
  11.688 -		(string_of_int ngoals ^ " unsolved goals!")
  11.689 -            else if (not (null hyps) andalso (not (in_locale hyps sign)))
  11.690 -		 then !result_error_fn state
  11.691 -                  ("Additional hypotheses:\n" ^ 
  11.692 -		   cat_lines 
  11.693 -		    (map (Sign.string_of_term sign) 
  11.694 -		     (List.filter (fn x => (not (in_locale [x] sign))) 
  11.695 -		      hyps)))
  11.696 -	    else if Pattern.matches (Sign.tsig_of sign)
  11.697 -			            (Envir.beta_norm (term_of chorn), Envir.beta_norm prop)
  11.698 -		 then final_th
  11.699 -	    else  !result_error_fn state "proved a different theorem"
  11.700 +                (string_of_int ngoals ^ " unsolved goals!")
  11.701 +            else if (not (null hyps) andalso (not (in_locale hyps thy)))
  11.702 +                 then !result_error_fn state
  11.703 +                  ("Additional hypotheses:\n" ^
  11.704 +                   cat_lines
  11.705 +                    (map (Sign.string_of_term thy)
  11.706 +                     (List.filter (fn x => (not (in_locale [x] thy)))
  11.707 +                      hyps)))
  11.708 +            else if Pattern.matches (Sign.tsig_of thy)
  11.709 +                                    (Envir.beta_norm (term_of chorn), Envir.beta_norm prop)
  11.710 +                 then final_th
  11.711 +            else  !result_error_fn state "proved a different theorem"
  11.712          end
  11.713    in
  11.714 -     if Sign.eq_sg(sign, Thm.sign_of_thm st0)
  11.715 +     if eq_thy(thy, Thm.theory_of_thm st0)
  11.716       then (prems, st0, mkresult)
  11.717 -     else error ("Definitions would change the proof state's signature" ^
  11.718 -		 sign_error (sign, Thm.sign_of_thm st0))
  11.719 +     else error ("Definitions would change the proof state's theory" ^
  11.720 +                 thy_error (thy, Thm.theory_of_thm st0))
  11.721    end
  11.722    handle THM(s,_,_) => error("prepare_proof: exception THM was raised!\n" ^ s);
  11.723  
  11.724  (*Prints exceptions readably to users*)
  11.725 -fun print_sign_exn_unit sign e = 
  11.726 +fun print_sign_exn_unit thy e =
  11.727    case e of
  11.728       THM (msg,i,thms) =>
  11.729 -	 (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
  11.730 -	  List.app print_thm thms)
  11.731 +         (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
  11.732 +          List.app print_thm thms)
  11.733     | THEORY (msg,thys) =>
  11.734 -	 (writeln ("Exception THEORY raised:\n" ^ msg);
  11.735 -	  List.app (Pretty.writeln o Display.pretty_theory) thys)
  11.736 +         (writeln ("Exception THEORY raised:\n" ^ msg);
  11.737 +          List.app (writeln o Context.str_of_thy) thys)
  11.738     | TERM (msg,ts) =>
  11.739 -	 (writeln ("Exception TERM raised:\n" ^ msg);
  11.740 -	  List.app (writeln o Sign.string_of_term sign) ts)
  11.741 +         (writeln ("Exception TERM raised:\n" ^ msg);
  11.742 +          List.app (writeln o Sign.string_of_term thy) ts)
  11.743     | TYPE (msg,Ts,ts) =>
  11.744 -	 (writeln ("Exception TYPE raised:\n" ^ msg);
  11.745 -	  List.app (writeln o Sign.string_of_typ sign) Ts;
  11.746 -	  List.app (writeln o Sign.string_of_term sign) ts)
  11.747 +         (writeln ("Exception TYPE raised:\n" ^ msg);
  11.748 +          List.app (writeln o Sign.string_of_typ thy) Ts;
  11.749 +          List.app (writeln o Sign.string_of_term thy) ts)
  11.750     | e => raise e;
  11.751  
  11.752  (*Prints an exception, then fails*)
  11.753 -fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise ERROR);
  11.754 +fun print_sign_exn thy e = (print_sign_exn_unit thy e; raise ERROR);
  11.755  
  11.756  (** the prove_goal.... commands
  11.757      Prove theorem using the listed tactics; check it has the specified form.
  11.758 -    Augment signature with all type assignments of goal.
  11.759 +    Augment theory with all type assignments of goal.
  11.760      Syntax is similar to "goal" command for easy keyboard use. **)
  11.761  
  11.762  (*Version taking the goal as a cterm*)
  11.763  fun prove_goalw_cterm_general check rths chorn tacsf =
  11.764    let val (prems, st0, mkresult) = prepare_proof false rths chorn
  11.765        val tac = EVERY (tacsf prems)
  11.766 -      fun statef() = 
  11.767 -	  (case Seq.pull (tac st0) of 
  11.768 -	       SOME(st,_) => st
  11.769 -	     | _ => error ("prove_goal: tactic failed"))
  11.770 +      fun statef() =
  11.771 +          (case Seq.pull (tac st0) of
  11.772 +               SOME(st,_) => st
  11.773 +             | _ => error ("prove_goal: tactic failed"))
  11.774    in  mkresult (check, cond_timeit (!Output.timing) statef)  end
  11.775 -  handle e => (print_sign_exn_unit (#sign (rep_cterm chorn)) e;
  11.776 -	       writeln ("The exception above was raised for\n" ^ 
  11.777 -		      Display.string_of_cterm chorn); raise e);
  11.778 +  handle e => (print_sign_exn_unit (#thy (rep_cterm chorn)) e;
  11.779 +               writeln ("The exception above was raised for\n" ^
  11.780 +                      Display.string_of_cterm chorn); raise e);
  11.781  
  11.782 -(*Two variants: one checking the result, one not.  
  11.783 +(*Two variants: one checking the result, one not.
  11.784    Neither prints runtime messages: they are for internal packages.*)
  11.785 -fun prove_goalw_cterm rths chorn = 
  11.786 -	setmp Output.timing false (prove_goalw_cterm_general true rths chorn)
  11.787 -and prove_goalw_cterm_nocheck rths chorn = 
  11.788 -	setmp Output.timing false (prove_goalw_cterm_general false rths chorn);
  11.789 +fun prove_goalw_cterm rths chorn =
  11.790 +        setmp Output.timing false (prove_goalw_cterm_general true rths chorn)
  11.791 +and prove_goalw_cterm_nocheck rths chorn =
  11.792 +        setmp Output.timing false (prove_goalw_cterm_general false rths chorn);
  11.793  
  11.794  
  11.795  (*Version taking the goal as a string*)
  11.796  fun prove_goalw thy rths agoal tacsf =
  11.797 -  let val sign = Theory.sign_of thy
  11.798 -      val chorn = read_cterm sign (agoal,propT)
  11.799 -  in  prove_goalw_cterm_general true rths chorn tacsf end
  11.800 +  let val chorn = read_cterm thy (agoal, propT)
  11.801 +  in prove_goalw_cterm_general true rths chorn tacsf end
  11.802    handle ERROR => error (*from read_cterm?*)
  11.803 -		("The error(s) above occurred for " ^ quote agoal);
  11.804 +                ("The error(s) above occurred for " ^ quote agoal);
  11.805  
  11.806  (*String version with no meta-rewrite-rules*)
  11.807  fun prove_goal thy = prove_goalw thy [];
  11.808 @@ -847,7 +831,7 @@
  11.809  (*** Commands etc ***)
  11.810  
  11.811  (*Return the current goal stack, if any, from undo_list*)
  11.812 -fun getstate() : gstack = case !undo_list of 
  11.813 +fun getstate() : gstack = case !undo_list of
  11.814        []   => error"No current state in subgoal module"
  11.815      | x::_ => x;
  11.816  
  11.817 @@ -868,7 +852,7 @@
  11.818  
  11.819  (*Printing can raise exceptions, so the assignment occurs last.
  11.820    Can do   setstate[(st,Seq.empty)]  to set st as the state.  *)
  11.821 -fun setstate newgoals = 
  11.822 +fun setstate newgoals =
  11.823    (print_top (pop newgoals);  undo_list := newgoals :: !undo_list);
  11.824  
  11.825  (*Given a proof state transformation, return a command that updates
  11.826 @@ -895,7 +879,7 @@
  11.827    For debugging uses of METAHYPS*)
  11.828  local exception GETHYPS of thm list
  11.829  in
  11.830 -fun gethyps i = 
  11.831 +fun gethyps i =
  11.832      (METAHYPS (fn hyps => raise (GETHYPS hyps)) i (topthm());  [])
  11.833      handle GETHYPS hyps => hyps
  11.834  end;
  11.835 @@ -904,14 +888,14 @@
  11.836  fun filter_goal could ths i = filter_thms could (999, getgoal i, ths);
  11.837  
  11.838  (*For inspecting earlier levels of the backward proof*)
  11.839 -fun chop_level n (pair,pairs) = 
  11.840 +fun chop_level n (pair,pairs) =
  11.841    let val level = length pairs
  11.842    in  if n<0 andalso ~n <= level
  11.843 -      then  List.drop (pair::pairs, ~n) 
  11.844 +      then  List.drop (pair::pairs, ~n)
  11.845        else if 0<=n andalso n<= level
  11.846 -      then  List.drop (pair::pairs, level - n) 
  11.847 -      else  error ("Level number must lie between 0 and " ^ 
  11.848 -		   string_of_int level)
  11.849 +      then  List.drop (pair::pairs, level - n)
  11.850 +      else  error ("Level number must lie between 0 and " ^
  11.851 +                   string_of_int level)
  11.852    end;
  11.853  
  11.854  (*Print the given level of the proof; prlev ~1 prints previous level*)
  11.855 @@ -922,15 +906,15 @@
  11.856  fun prlim n = (goals_limit:=n; pr());
  11.857  
  11.858  (** the goal.... commands
  11.859 -    Read main goal.  Set global variables curr_prems, curr_mkresult. 
  11.860 +    Read main goal.  Set global variables curr_prems, curr_mkresult.
  11.861      Initial subgoal and premises are rewritten using rths. **)
  11.862  
  11.863  (*Version taking the goal as a cterm; if you have a term t and theory thy, use
  11.864 -    goalw_cterm rths (cterm_of (Theory.sign_of thy) t);      *)
  11.865 -fun agoalw_cterm atomic rths chorn = 
  11.866 +    goalw_cterm rths (cterm_of thy t);      *)
  11.867 +fun agoalw_cterm atomic rths chorn =
  11.868    let val (prems, st0, mkresult) = prepare_proof atomic rths chorn
  11.869    in  undo_list := [];
  11.870 -      setstate [ (st0, Seq.empty) ];  
  11.871 +      setstate [ (st0, Seq.empty) ];
  11.872        curr_prems := prems;
  11.873        curr_mkresult := mkresult;
  11.874        prems
  11.875 @@ -939,10 +923,10 @@
  11.876  val goalw_cterm = agoalw_cterm false;
  11.877  
  11.878  (*Version taking the goal as a string*)
  11.879 -fun agoalw atomic thy rths agoal = 
  11.880 -    agoalw_cterm atomic rths (read_cterm(Theory.sign_of thy)(agoal,propT))
  11.881 +fun agoalw atomic thy rths agoal =
  11.882 +    agoalw_cterm atomic rths (read_cterm thy (agoal, propT))
  11.883      handle ERROR => error (*from type_assign, etc via prepare_proof*)
  11.884 -	("The error(s) above occurred for " ^ quote agoal);
  11.885 +        ("The error(s) above occurred for " ^ quote agoal);
  11.886  
  11.887  val goalw = agoalw false;
  11.888  
  11.889 @@ -978,15 +962,15 @@
  11.890  fun by_com tac ((th,ths), pairs) : gstack =
  11.891    (case  Seq.pull(tac th)  of
  11.892       NONE      => error"by: tactic failed"
  11.893 -   | SOME(th2,ths2) => 
  11.894 -       (if eq_thm(th,th2) 
  11.895 -	  then warning "Warning: same as previous level"
  11.896 -	  else if eq_thm_sg(th,th2) then ()
  11.897 -	  else warning ("Warning: signature of proof state has changed" ^
  11.898 -		       sign_error (Thm.sign_of_thm th, Thm.sign_of_thm th2));
  11.899 +   | SOME(th2,ths2) =>
  11.900 +       (if eq_thm(th,th2)
  11.901 +          then warning "Warning: same as previous level"
  11.902 +          else if eq_thm_thy(th,th2) then ()
  11.903 +          else warning ("Warning: theory of proof state has changed" ^
  11.904 +                       thy_error (Thm.theory_of_thm th, Thm.theory_of_thm th2));
  11.905         ((th2,ths2)::(th,ths)::pairs)));
  11.906  
  11.907 -fun by tac = cond_timeit (!Output.timing) 
  11.908 +fun by tac = cond_timeit (!Output.timing)
  11.909      (fn() => make_command (by_com tac));
  11.910  
  11.911  (* byev[tac1,...,tacn] applies tac1 THEN ... THEN tacn.
  11.912 @@ -999,13 +983,13 @@
  11.913  fun backtrack [] = error"back: no alternatives"
  11.914    | backtrack ((th,thstr) :: pairs) =
  11.915       (case Seq.pull thstr of
  11.916 -	  NONE      => (writeln"Going back a level..."; backtrack pairs)
  11.917 -	| SOME(th2,thstr2) =>  
  11.918 -	   (if eq_thm(th,th2) 
  11.919 -	      then warning "Warning: same as previous choice at this level"
  11.920 -	      else if eq_thm_sg(th,th2) then ()
  11.921 -	      else warning "Warning: signature of proof state has changed";
  11.922 -	    (th2,thstr2)::pairs));
  11.923 +          NONE      => (writeln"Going back a level..."; backtrack pairs)
  11.924 +        | SOME(th2,thstr2) =>
  11.925 +           (if eq_thm(th,th2)
  11.926 +              then warning "Warning: same as previous choice at this level"
  11.927 +              else if eq_thm_thy(th,th2) then ()
  11.928 +              else warning "Warning: theory of proof state has changed";
  11.929 +            (th2,thstr2)::pairs));
  11.930  
  11.931  fun back() = setstate (backtrack (getstate()));
  11.932  
  11.933 @@ -1031,25 +1015,25 @@
  11.934  
  11.935  
  11.936  fun top_proof() = case !proofstack of
  11.937 -	[] => error("Stack of proof attempts is empty!")
  11.938 +        [] => error("Stack of proof attempts is empty!")
  11.939      | p::ps => (p,ps);
  11.940  
  11.941  (*  push a copy of the current proof state on to the stack *)
  11.942  fun push_proof() = (proofstack := (save_proof() :: !proofstack));
  11.943  
  11.944  (* discard the top proof state of the stack *)
  11.945 -fun pop_proof() = 
  11.946 +fun pop_proof() =
  11.947    let val (p,ps) = top_proof()
  11.948        val prems = restore_proof p
  11.949    in proofstack := ps;  pr();  prems end;
  11.950  
  11.951  (* rotate the stack so that the top element goes to the bottom *)
  11.952  fun rotate_proof() = let val (p,ps) = top_proof()
  11.953 -		    in proofstack := ps@[save_proof()];
  11.954 -		       restore_proof p;
  11.955 -		       pr();
  11.956 -		       !curr_prems
  11.957 -		    end;
  11.958 +                    in proofstack := ps@[save_proof()];
  11.959 +                       restore_proof p;
  11.960 +                       pr();
  11.961 +                       !curr_prems
  11.962 +                    end;
  11.963  
  11.964  
  11.965  (** Shortcuts for commonly-used tactics **)
  11.966 @@ -1085,11 +1069,11 @@
  11.967  
  11.968  (** Reading and printing terms wrt the current theory **)
  11.969  
  11.970 -fun top_sg() = Thm.sign_of_thm (topthm());
  11.971 +fun top_sg() = Thm.theory_of_thm (topthm());
  11.972  
  11.973  fun read s = term_of (read_cterm (top_sg()) (s, TypeInfer.logicT));
  11.974  
  11.975 -(*Print a term under the current signature of the proof state*)
  11.976 +(*Print a term under the current theory of the proof state*)
  11.977  fun prin t = writeln (Sign.string_of_term (top_sg()) t);
  11.978  
  11.979  fun printyp T = writeln (Sign.string_of_typ (top_sg()) T);
  11.980 @@ -1099,7 +1083,7 @@
  11.981  fun pprint_typ T = Sign.pprint_typ (top_sg()) T;
  11.982  
  11.983  
  11.984 -(*Prints exceptions nicely at top level; 
  11.985 +(*Prints exceptions nicely at top level;
  11.986    raises the exception in order to have a polymorphic type!*)
  11.987  fun print_exn e = (print_sign_exn_unit (top_sg()) e;  raise e);
  11.988  
  11.989 @@ -1128,15 +1112,15 @@
  11.990  
  11.991  (* retrieval *)
  11.992  
  11.993 -fun theory_of_goal () = ThyInfo.theory_of_sign (Thm.sign_of_thm (topthm ()));
  11.994 +fun theory_of_goal () = Thm.theory_of_thm (topthm ());
  11.995  val context_of_goal = ProofContext.init o theory_of_goal;
  11.996  
  11.997  fun thms_containing raw_consts =
  11.998    let
  11.999      val thy = theory_of_goal ();
 11.1000 -    val consts = map (Sign.intern_const (Theory.sign_of thy)) raw_consts;
 11.1001 +    val consts = map (Sign.intern_const thy) raw_consts;
 11.1002    in
 11.1003 -    (case List.filter (is_none o Sign.const_type (Theory.sign_of thy)) consts of
 11.1004 +    (case List.filter (is_none o Sign.const_type thy) consts of
 11.1005        [] => ()
 11.1006      | cs => error ("thms_containing: undeclared consts " ^ commas_quote cs));
 11.1007      PureThy.thms_containing_consts thy consts
    12.1 --- a/src/Pure/meta_simplifier.ML	Fri Jun 17 18:33:42 2005 +0200
    12.2 +++ b/src/Pure/meta_simplifier.ML	Fri Jun 17 18:35:27 2005 +0200
    12.3 @@ -42,7 +42,7 @@
    12.4    val merge_ss: simpset * simpset -> simpset
    12.5    type simproc
    12.6    val mk_simproc: string -> cterm list ->
    12.7 -    (Sign.sg -> simpset -> term -> thm option) -> simproc
    12.8 +    (theory -> simpset -> term -> thm option) -> simproc
    12.9    val add_prems: thm list -> simpset -> simpset
   12.10    val prems_of_ss: simpset -> thm list
   12.11    val addsimps: simpset * thm list -> simpset
   12.12 @@ -75,15 +75,15 @@
   12.13    exception SIMPLIFIER of string * thm
   12.14    val clear_ss: simpset -> simpset
   12.15    exception SIMPROC_FAIL of string * exn
   12.16 -  val simproc_i: Sign.sg -> string -> term list
   12.17 -    -> (Sign.sg -> simpset -> term -> thm option) -> simproc
   12.18 -  val simproc: Sign.sg -> string -> string list
   12.19 -    -> (Sign.sg -> simpset -> term -> thm option) -> simproc
   12.20 +  val simproc_i: theory -> string -> term list
   12.21 +    -> (theory -> simpset -> term -> thm option) -> simproc
   12.22 +  val simproc: theory -> string -> string list
   12.23 +    -> (theory -> simpset -> term -> thm option) -> simproc
   12.24    val rewrite_cterm: bool * bool * bool ->
   12.25      (simpset -> thm -> thm option) -> simpset -> cterm -> thm
   12.26    val rewrite_aux: (simpset -> thm -> thm option) -> bool -> thm list -> cterm -> thm
   12.27    val simplify_aux: (simpset -> thm -> thm option) -> bool -> thm list -> thm -> thm
   12.28 -  val rewrite_term: Sign.sg -> thm list -> (term -> term option) list -> term -> term
   12.29 +  val rewrite_term: theory -> thm list -> (term -> term option) list -> term -> term
   12.30    val rewrite_thm: bool * bool * bool ->
   12.31      (simpset -> thm -> thm option) -> simpset -> thm -> thm
   12.32    val rewrite_goals_rule_aux: (simpset -> thm -> thm option) -> thm list -> thm -> thm
   12.33 @@ -116,7 +116,7 @@
   12.34    else tracing (enclose "[" "]" (string_of_int(!simp_depth)) ^ a);
   12.35  
   12.36  fun prnt warn a = if warn then warning a else println a;
   12.37 -fun prtm warn a sg t = prnt warn (a ^ "\n" ^ Sign.string_of_term sg t);
   12.38 +fun prtm warn a thy t = prnt warn (a ^ "\n" ^ Sign.string_of_term thy t);
   12.39  fun prctm warn a t = prnt warn (a ^ "\n" ^ Display.string_of_cterm t);
   12.40  
   12.41  in
   12.42 @@ -124,8 +124,8 @@
   12.43  fun debug warn a = if ! debug_simp then prnt warn a else ();
   12.44  fun trace warn a = if ! trace_simp then prnt warn a else ();
   12.45  
   12.46 -fun debug_term warn a sign t = if ! debug_simp then prtm warn a sign t else ();
   12.47 -fun trace_term warn a sign t = if ! trace_simp then prtm warn a sign t else ();
   12.48 +fun debug_term warn a thy t = if ! debug_simp then prtm warn a thy t else ();
   12.49 +fun trace_term warn a thy t = if ! trace_simp then prtm warn a thy t else ();
   12.50  fun trace_cterm warn a ct = if ! trace_simp then prctm warn a ct else ();
   12.51  fun trace_thm a th = if ! trace_simp then prctm false a (Thm.cprop_of th) else ();
   12.52  
   12.53 @@ -231,7 +231,7 @@
   12.54    Proc of
   12.55     {name: string,
   12.56      lhs: cterm,
   12.57 -    proc: Sign.sg -> simpset -> term -> thm option,
   12.58 +    proc: theory -> simpset -> term -> thm option,
   12.59      id: stamp};
   12.60  
   12.61  fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = (id1 = id2);
   12.62 @@ -354,8 +354,8 @@
   12.63        Proc {name = name, lhs = lhs, proc = proc, id = id}))
   12.64    end;
   12.65  
   12.66 -fun simproc_i sg name = mk_simproc name o map (Thm.cterm_of sg o Logic.varify);
   12.67 -fun simproc sg name = simproc_i sg name o map (Sign.simple_read_term sg TypeInfer.logicT);
   12.68 +fun simproc_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify);
   12.69 +fun simproc thy name = simproc_i thy name o map (Sign.simple_read_term thy TypeInfer.logicT);
   12.70  
   12.71  
   12.72  
   12.73 @@ -407,7 +407,7 @@
   12.74    not (term_tvars erhs subset (term_tvars elhs union List.concat (map term_tvars prems)));
   12.75  
   12.76  (*simple test for looping rewrite rules and stupid orientations*)
   12.77 -fun reorient sign prems lhs rhs =
   12.78 +fun reorient thy prems lhs rhs =
   12.79    rewrite_rule_extra_vars prems lhs rhs
   12.80      orelse
   12.81    is_Var (head_of lhs)
   12.82 @@ -420,7 +420,7 @@
   12.83  *)
   12.84    exists (apl (lhs, Logic.occs)) (rhs :: prems)
   12.85      orelse
   12.86 -  null prems andalso Pattern.matches (Sign.tsig_of sign) (lhs, rhs)
   12.87 +  null prems andalso Pattern.matches (Sign.tsig_of thy) (lhs, rhs)
   12.88      (*the condition "null prems" is necessary because conditional rewrites
   12.89        with extra variables in the conditions may terminate although
   12.90        the rhs is an instance of the lhs; example: ?m < ?n ==> f(?n) == f(?m)*)
   12.91 @@ -429,7 +429,7 @@
   12.92  
   12.93  fun decomp_simp thm =
   12.94    let
   12.95 -    val {sign, prop, ...} = Thm.rep_thm thm;
   12.96 +    val {thy, prop, ...} = Thm.rep_thm thm;
   12.97      val prems = Logic.strip_imp_prems prop;
   12.98      val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
   12.99      val (lhs, rhs) = Drule.dest_equals concl handle TERM _ =>
  12.100 @@ -441,7 +441,7 @@
  12.101        var_perm (term_of elhs, erhs) andalso
  12.102        not (term_of elhs aconv erhs) andalso
  12.103        not (is_Var (term_of elhs));
  12.104 -  in (sign, prems, term_of lhs, elhs, term_of rhs, perm) end;
  12.105 +  in (thy, prems, term_of lhs, elhs, term_of rhs, perm) end;
  12.106  
  12.107  fun decomp_simp' thm =
  12.108    let val (_, _, lhs, _, rhs, _) = decomp_simp thm in
  12.109 @@ -476,10 +476,10 @@
  12.110    end;
  12.111  
  12.112  fun orient_rrule ss (thm, name) =
  12.113 -  let val (sign, prems, lhs, elhs, rhs, perm) = decomp_simp thm in
  12.114 +  let val (thy, prems, lhs, elhs, rhs, perm) = decomp_simp thm in
  12.115      if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
  12.116 -    else if reorient sign prems lhs rhs then
  12.117 -      if reorient sign prems rhs lhs
  12.118 +    else if reorient thy prems lhs rhs then
  12.119 +      if reorient thy prems rhs lhs
  12.120        then mk_eq_True ss (thm, name)
  12.121        else
  12.122          let val Simpset (_, {mk_rews = {mk_sym, ...}, ...}) = ss in
  12.123 @@ -718,9 +718,9 @@
  12.124        (symmetric (Drule.beta_eta_conversion (lhs_of thm'))) thm')
  12.125    in if msg then trace_thm "SUCCEEDED" thm' else (); SOME thm'' end
  12.126    handle THM _ =>
  12.127 -    let val {sign, prop = _ $ _ $ prop0, ...} = Thm.rep_thm thm in
  12.128 +    let val {thy, prop = _ $ _ $ prop0, ...} = Thm.rep_thm thm in
  12.129        trace_thm "Proved wrong thm (Check subgoaler?)" thm';
  12.130 -      trace_term false "Should have proved:" sign prop0;
  12.131 +      trace_term false "Should have proved:" thy prop0;
  12.132        NONE
  12.133      end;
  12.134  
  12.135 @@ -773,16 +773,16 @@
  12.136    IMPORTANT: rewrite rules must not introduce new Vars or TVars!
  12.137  *)
  12.138  
  12.139 -fun rewritec (prover, signt, maxt) ss t =
  12.140 +fun rewritec (prover, thyt, maxt) ss t =
  12.141    let
  12.142      val Simpset ({rules, ...}, {congs, procs, termless, ...}) = ss;
  12.143      val eta_thm = Thm.eta_conversion t;
  12.144      val eta_t' = rhs_of eta_thm;
  12.145      val eta_t = term_of eta_t';
  12.146 -    val tsigt = Sign.tsig_of signt;
  12.147 +    val tsigt = Sign.tsig_of thyt;
  12.148      fun rew {thm, name, lhs, elhs, fo, perm} =
  12.149        let
  12.150 -        val {sign, prop, maxidx, ...} = rep_thm thm;
  12.151 +        val {thy, prop, maxidx, ...} = rep_thm thm;
  12.152          val (rthm, elhs') = if maxt = ~1 then (thm, elhs)
  12.153            else (Thm.incr_indexes (maxt+1) thm, Thm.cterm_incr_indexes (maxt+1) elhs);
  12.154          val insts = if fo then Thm.cterm_first_order_match (elhs', eta_t')
  12.155 @@ -837,9 +837,9 @@
  12.156      fun proc_rews [] = NONE
  12.157        | proc_rews (Proc {name, proc, lhs, ...} :: ps) =
  12.158            if Pattern.matches tsigt (Thm.term_of lhs, Thm.term_of t) then
  12.159 -            (debug_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t;
  12.160 +            (debug_term false ("Trying procedure " ^ quote name ^ " on:") thyt eta_t;
  12.161               case transform_failure (curry SIMPROC_FAIL name)
  12.162 -                 (fn () => proc signt ss eta_t) () of
  12.163 +                 (fn () => proc thyt ss eta_t) () of
  12.164                 NONE => (debug false "FAILED"; proc_rews ps)
  12.165               | SOME raw_thm =>
  12.166                   (trace_thm ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm;
  12.167 @@ -859,8 +859,8 @@
  12.168  
  12.169  (* conversion to apply a congruence rule to a term *)
  12.170  
  12.171 -fun congc (prover,signt,maxt) {thm=cong,lhs=lhs} t =
  12.172 -  let val sign = Thm.sign_of_thm cong
  12.173 +fun congc (prover,thyt,maxt) {thm=cong,lhs=lhs} t =
  12.174 +  let val thy = Thm.theory_of_thm cong
  12.175        val rthm = if maxt = ~1 then cong else Thm.incr_indexes (maxt+1) cong;
  12.176        val rlhs = fst (Drule.dest_equals (Drule.strip_imp_concl (cprop_of rthm)));
  12.177        val insts = Thm.cterm_match (rlhs, t)
  12.178 @@ -889,20 +889,20 @@
  12.179  fun transitive2 thm = transitive1 (SOME thm);
  12.180  fun transitive3 thm = transitive1 thm o SOME;
  12.181  
  12.182 -fun bottomc ((simprem, useprem, mutsimp), prover, sign, maxidx) =
  12.183 +fun bottomc ((simprem, useprem, mutsimp), prover, thy, maxidx) =
  12.184    let
  12.185      fun botc skel ss t =
  12.186            if is_Var skel then NONE
  12.187            else
  12.188            (case subc skel ss t of
  12.189               some as SOME thm1 =>
  12.190 -               (case rewritec (prover, sign, maxidx) ss (rhs_of thm1) of
  12.191 +               (case rewritec (prover, thy, maxidx) ss (rhs_of thm1) of
  12.192                    SOME (thm2, skel2) =>
  12.193                      transitive2 (transitive thm1 thm2)
  12.194                        (botc skel2 ss (rhs_of thm2))
  12.195                  | NONE => some)
  12.196             | NONE =>
  12.197 -               (case rewritec (prover, sign, maxidx) ss t of
  12.198 +               (case rewritec (prover, thy, maxidx) ss t of
  12.199                    SOME (thm2, skel2) => transitive2 thm2
  12.200                      (botc skel2 ss (rhs_of thm2))
  12.201                  | NONE => NONE))
  12.202 @@ -957,7 +957,7 @@
  12.203    (*post processing: some partial applications h t1 ... tj, j <= length ts,
  12.204      may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*)
  12.205                            (let
  12.206 -                             val thm = congc (prover ss, sign, maxidx) cong t0;
  12.207 +                             val thm = congc (prover ss, thy, maxidx) cong t0;
  12.208                               val t = getOpt (Option.map rhs_of thm, t0);
  12.209                               val (cl, cr) = Thm.dest_comb t
  12.210                               val dVar = Var(("", 0), dummyT)
  12.211 @@ -1012,7 +1012,7 @@
  12.212              val concl' =
  12.213                Drule.mk_implies (prem, getOpt (Option.map rhs_of eq, concl));
  12.214              val dprem = Option.map (curry (disch false) prem)
  12.215 -          in case rewritec (prover, sign, maxidx) ss' concl' of
  12.216 +          in case rewritec (prover, thy, maxidx) ss' concl' of
  12.217                NONE => rebuild prems concl' rrss asms ss (dprem eq)
  12.218              | SOME (eq', _) => transitive2 (Library.foldl (disch false o swap)
  12.219                    (valOf (transitive3 (dprem eq) eq'), prems))
  12.220 @@ -1096,8 +1096,8 @@
  12.221     then warning ("Simplification depth " ^ string_of_int (!simp_depth))
  12.222     else ();
  12.223     trace_cterm false "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" ct;
  12.224 -   let val {sign, t, maxidx, ...} = Thm.rep_cterm ct
  12.225 -       val res = bottomc (mode, prover, sign, maxidx) ss ct
  12.226 +   let val {thy, t, maxidx, ...} = Thm.rep_cterm ct
  12.227 +       val res = bottomc (mode, prover, thy, maxidx) ss ct
  12.228           handle THM (s, _, thms) =>
  12.229           error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^
  12.230             Pretty.string_of (Display.pretty_thms thms))
  12.231 @@ -1115,8 +1115,8 @@
  12.232        Drule.fconv_rule (rewrite_cterm (full, false, false) prover (empty_ss addsimps thms));
  12.233  
  12.234  (*simple term rewriting -- no proof*)
  12.235 -fun rewrite_term sg rules procs =
  12.236 -  Pattern.rewrite_term (Sign.tsig_of sg) (map decomp_simp' rules) procs;
  12.237 +fun rewrite_term thy rules procs =
  12.238 +  Pattern.rewrite_term (Sign.tsig_of thy) (map decomp_simp' rules) procs;
  12.239  
  12.240  fun rewrite_thm mode prover ss = Drule.fconv_rule (rewrite_cterm mode prover ss);
  12.241  
    13.1 --- a/src/Pure/proofterm.ML	Fri Jun 17 18:33:42 2005 +0200
    13.2 +++ b/src/Pure/proofterm.ML	Fri Jun 17 18:35:27 2005 +0200
    13.3 @@ -95,7 +95,7 @@
    13.4    val equal_elim : term -> term -> proof -> proof -> proof
    13.5    val axm_proof : string -> term -> proof
    13.6    val oracle_proof : string -> term -> proof
    13.7 -  val thm_proof : Sign.sg -> string * (string * string list) list ->
    13.8 +  val thm_proof : theory -> string * (string * string list) list ->
    13.9      term list -> term -> proof -> proof
   13.10    val get_name_tags : term list -> term -> proof -> string * (string * string list) list
   13.11  
   13.12 @@ -1093,21 +1093,19 @@
   13.13  
   13.14  (* data kind 'Pure/proof' *)
   13.15  
   13.16 -structure ProofArgs =
   13.17 -struct
   13.18 +structure ProofData = TheoryDataFun
   13.19 +(struct
   13.20    val name = "Pure/proof";
   13.21    type T = ((proof * proof) list *
   13.22      (string * (typ list -> proof -> proof option)) list);
   13.23  
   13.24    val empty = ([], []);
   13.25    val copy = I;
   13.26 -  val prep_ext = I;
   13.27 -  fun merge ((rules1, procs1), (rules2, procs2)) =
   13.28 +  val extend = I;
   13.29 +  fun merge _ ((rules1, procs1), (rules2, procs2)) =
   13.30      (merge_lists rules1 rules2, merge_alists procs1 procs2);
   13.31    fun print _ _ = ();
   13.32 -end;
   13.33 -
   13.34 -structure ProofData = TheoryDataFun(ProofArgs);
   13.35 +end);
   13.36  
   13.37  val init = ProofData.init;
   13.38  
   13.39 @@ -1119,7 +1117,7 @@
   13.40    let val r = ProofData.get thy
   13.41    in ProofData.put (fst r, ps @ snd r) thy end;
   13.42  
   13.43 -fun thm_proof sign (name, tags) hyps prop prf =
   13.44 +fun thm_proof thy (name, tags) hyps prop prf =
   13.45    let
   13.46      val prop = Logic.list_implies (hyps, prop);
   13.47      val nvs = needed_vars prop;
   13.48 @@ -1127,7 +1125,7 @@
   13.49          if ixn mem nvs then SOME v else NONE) (vars_of prop) @
   13.50        map SOME (sort (make_ord atless) (term_frees prop));
   13.51      val opt_prf = if ! proofs = 2 then
   13.52 -        #4 (shrink [] 0 (rewrite_prf fst (ProofData.get_sg sign)
   13.53 +        #4 (shrink [] 0 (rewrite_prf fst (ProofData.get thy)
   13.54            (foldr (uncurry implies_intr_proof) prf hyps)))
   13.55        else MinProof (mk_min_proof ([], prf));
   13.56      val head = (case strip_combt (fst (strip_combP prf)) of
    14.1 --- a/src/Pure/simplifier.ML	Fri Jun 17 18:33:42 2005 +0200
    14.2 +++ b/src/Pure/simplifier.ML	Fri Jun 17 18:35:27 2005 +0200
    14.3 @@ -22,9 +22,9 @@
    14.4    val mk_context_simproc: string -> cterm list ->
    14.5      (Proof.context -> simpset -> term -> thm option) -> context_simproc
    14.6    val print_simpset: theory -> unit
    14.7 -  val simpset_ref_of_sg: Sign.sg -> simpset ref
    14.8 +  val simpset_ref_of_sg: theory -> simpset ref    (*obsolete*)
    14.9    val simpset_ref_of: theory -> simpset ref
   14.10 -  val simpset_of_sg: Sign.sg -> simpset
   14.11 +  val simpset_of_sg: theory -> simpset            (*obsolete*)
   14.12    val simpset_of: theory -> simpset
   14.13    val SIMPSET: (simpset -> tactic) -> tactic
   14.14    val SIMPSET': (simpset -> 'a -> tactic) -> 'a -> tactic
   14.15 @@ -58,13 +58,13 @@
   14.16  signature SIMPLIFIER =
   14.17  sig
   14.18    include BASIC_SIMPLIFIER
   14.19 -  val simproc_i: Sign.sg -> string -> term list
   14.20 -    -> (Sign.sg -> simpset -> term -> thm option) -> simproc
   14.21 -  val simproc: Sign.sg -> string -> string list
   14.22 -    -> (Sign.sg -> simpset -> term -> thm option) -> simproc
   14.23 -  val context_simproc_i: Sign.sg -> string -> term list
   14.24 +  val simproc_i: theory -> string -> term list
   14.25 +    -> (theory -> simpset -> term -> thm option) -> simproc
   14.26 +  val simproc: theory -> string -> string list
   14.27 +    -> (theory -> simpset -> term -> thm option) -> simproc
   14.28 +  val context_simproc_i: theory -> string -> term list
   14.29      -> (Proof.context -> simpset -> term -> thm option) -> context_simproc
   14.30 -  val context_simproc: Sign.sg -> string -> string list
   14.31 +  val context_simproc: theory -> string -> string list
   14.32      -> (Proof.context -> simpset -> term -> thm option) -> context_simproc
   14.33    val          rewrite: simpset -> cterm -> thm
   14.34    val      asm_rewrite: simpset -> cterm -> thm
   14.35 @@ -130,11 +130,11 @@
   14.36  fun eq_context_simproc (ContextSimproc (_, id1), ContextSimproc (_, id2)) = (id1 = id2);
   14.37  val merge_context_simprocs = gen_merge_lists eq_context_simproc;
   14.38  
   14.39 -fun context_simproc_i sg name =
   14.40 -  mk_context_simproc name o map (Thm.cterm_of sg o Logic.varify);
   14.41 +fun context_simproc_i thy name =
   14.42 +  mk_context_simproc name o map (Thm.cterm_of thy o Logic.varify);
   14.43  
   14.44 -fun context_simproc sg name =
   14.45 -  context_simproc_i sg name o map (Sign.simple_read_term sg TypeInfer.logicT);
   14.46 +fun context_simproc thy name =
   14.47 +  context_simproc_i thy name o map (Sign.simple_read_term thy TypeInfer.logicT);
   14.48  
   14.49  
   14.50  (* datatype context_ss *)
   14.51 @@ -188,25 +188,24 @@
   14.52  
   14.53  (* theory data kind 'Pure/simpset' *)
   14.54  
   14.55 -structure GlobalSimpsetArgs =
   14.56 -struct
   14.57 +structure GlobalSimpset = TheoryDataFun
   14.58 +(struct
   14.59    val name = "Pure/simpset";
   14.60    type T = simpset ref * context_ss;
   14.61  
   14.62    val empty = (ref empty_ss, empty_context_ss);
   14.63    fun copy (ref ss, ctxt_ss) = (ref ss, ctxt_ss): T;            (*create new reference!*)
   14.64 -  val prep_ext = copy;
   14.65 -  fun merge ((ref ss1, ctxt_ss1), (ref ss2, ctxt_ss2)) =
   14.66 +  val extend = copy;
   14.67 +  fun merge _ ((ref ss1, ctxt_ss1), (ref ss2, ctxt_ss2)) =
   14.68      (ref (merge_ss (ss1, ss2)), merge_context_ss (ctxt_ss1, ctxt_ss2));
   14.69    fun print _ (ref ss, _) = print_ss ss;
   14.70 -end;
   14.71 +end);
   14.72  
   14.73 -structure GlobalSimpset = TheoryDataFun(GlobalSimpsetArgs);
   14.74  val _ = Context.add_setup [GlobalSimpset.init];
   14.75  val print_simpset = GlobalSimpset.print;
   14.76  
   14.77 -val simpset_ref_of_sg = #1 o GlobalSimpset.get_sg;
   14.78  val simpset_ref_of = #1 o GlobalSimpset.get;
   14.79 +val simpset_ref_of_sg = simpset_ref_of;
   14.80  val get_context_ss = #2 o GlobalSimpset.get o ProofContext.theory_of;
   14.81  
   14.82  fun map_context_ss f = GlobalSimpset.map (apsnd
   14.83 @@ -216,14 +215,14 @@
   14.84  
   14.85  (* access global simpset *)
   14.86  
   14.87 -val simpset_of_sg = ! o simpset_ref_of_sg;
   14.88 -val simpset_of = simpset_of_sg o Theory.sign_of;
   14.89 +val simpset_of = ! o simpset_ref_of;
   14.90 +val simpset_of_sg = simpset_of;
   14.91  
   14.92 -fun SIMPSET tacf state = tacf (simpset_of_sg (Thm.sign_of_thm state)) state;
   14.93 -fun SIMPSET' tacf i state = tacf (simpset_of_sg (Thm.sign_of_thm state)) i state;
   14.94 +fun SIMPSET tacf state = tacf (simpset_of (Thm.theory_of_thm state)) state;
   14.95 +fun SIMPSET' tacf i state = tacf (simpset_of (Thm.theory_of_thm state)) i state;
   14.96  
   14.97  val simpset = simpset_of o Context.the_context;
   14.98 -val simpset_ref = simpset_ref_of_sg o Theory.sign_of o Context.the_context;
   14.99 +val simpset_ref = simpset_ref_of o Context.the_context;
  14.100  
  14.101  
  14.102  (* change global simpset *)
  14.103 @@ -285,15 +284,14 @@
  14.104  
  14.105  (* proof data kind 'Pure/simpset' *)
  14.106  
  14.107 -structure LocalSimpsetArgs =
  14.108 -struct
  14.109 +structure LocalSimpset = ProofDataFun
  14.110 +(struct
  14.111    val name = "Pure/simpset";
  14.112    type T = simpset;
  14.113    val init = simpset_of;
  14.114    fun print ctxt ss = print_ss (context_ss ctxt ss (get_context_ss ctxt));
  14.115 -end;
  14.116 +end);
  14.117  
  14.118 -structure LocalSimpset = ProofDataFun(LocalSimpsetArgs);
  14.119  val _ = Context.add_setup [LocalSimpset.init];
  14.120  val print_local_simpset = LocalSimpset.print;
  14.121  
    15.1 --- a/src/Sequents/prover.ML	Fri Jun 17 18:33:42 2005 +0200
    15.2 +++ b/src/Sequents/prover.ML	Fri Jun 17 18:35:27 2005 +0200
    15.3 @@ -168,32 +168,27 @@
    15.4  
    15.5  
    15.6  
    15.7 -structure ProverArgs =
    15.8 -  struct
    15.9 +structure ProverData = TheoryDataFun
   15.10 +(struct
   15.11    val name = "Sequents/prover";
   15.12    type T = pack ref;
   15.13    val empty = ref empty_pack
   15.14    fun copy (ref pack) = ref pack;
   15.15 -  val prep_ext = copy;
   15.16 -  fun merge (ref pack1, ref pack2) = ref (merge_pack (pack1, pack2));
   15.17 +  val extend = copy;
   15.18 +  fun merge _ (ref pack1, ref pack2) = ref (merge_pack (pack1, pack2));
   15.19    fun print _ (ref pack) = print_pack pack;
   15.20 -  end;
   15.21 -
   15.22 -structure ProverData = TheoryDataFun(ProverArgs);
   15.23 +end);
   15.24  
   15.25  val prover_setup = [ProverData.init];
   15.26  
   15.27  val print_pack = ProverData.print;
   15.28 -val pack_ref_of_sg = ProverData.get_sg;
   15.29  val pack_ref_of = ProverData.get;
   15.30  
   15.31  (* access global pack *)
   15.32  
   15.33 -val pack_of_sg = ! o pack_ref_of_sg;
   15.34 -val pack_of = pack_of_sg o sign_of;
   15.35 -
   15.36 +val pack_of = ! o pack_ref_of;
   15.37  val pack = pack_of o Context.the_context;
   15.38 -val pack_ref = pack_ref_of_sg o sign_of o Context.the_context;
   15.39 +val pack_ref = pack_ref_of o Context.the_context;
   15.40  
   15.41  
   15.42  (* change global pack *)
    16.1 --- a/src/ZF/Tools/induct_tacs.ML	Fri Jun 17 18:33:42 2005 +0200
    16.2 +++ b/src/ZF/Tools/induct_tacs.ML	Fri Jun 17 18:35:27 2005 +0200
    16.3 @@ -30,22 +30,20 @@
    16.4     mutual_induct : thm,
    16.5     exhaustion : thm};
    16.6  
    16.7 -structure DatatypesArgs =
    16.8 -  struct
    16.9 +structure DatatypesData = TheoryDataFun
   16.10 +(struct
   16.11    val name = "ZF/datatypes";
   16.12    type T = datatype_info Symtab.table;
   16.13  
   16.14    val empty = Symtab.empty;
   16.15    val copy = I;
   16.16 -  val prep_ext = I;
   16.17 -  val merge: T * T -> T = Symtab.merge (K true);
   16.18 +  val extend = I;
   16.19 +  fun merge _ tabs : T = Symtab.merge (K true) tabs;
   16.20  
   16.21 -  fun print sg tab =
   16.22 +  fun print thy tab =
   16.23      Pretty.writeln (Pretty.strs ("datatypes:" ::
   16.24 -      map #1 (NameSpace.extern_table (Sign.type_space sg, tab))));
   16.25 -  end;
   16.26 -
   16.27 -structure DatatypesData = TheoryDataFun(DatatypesArgs);
   16.28 +      map #1 (NameSpace.extern_table (Sign.type_space thy, tab))));
   16.29 +end);
   16.30  
   16.31  
   16.32  (** Constructor information: needed to map constructors to datatypes **)
   16.33 @@ -57,27 +55,22 @@
   16.34     rec_rewrites : thm list};  (*recursor equations*)
   16.35  
   16.36  
   16.37 -structure ConstructorsArgs =
   16.38 -struct
   16.39 +structure ConstructorsData = TheoryDataFun
   16.40 +(struct
   16.41    val name = "ZF/constructors"
   16.42    type T = constructor_info Symtab.table
   16.43 -
   16.44    val empty = Symtab.empty
   16.45    val copy = I;
   16.46 -  val prep_ext = I
   16.47 -  val merge: T * T -> T = Symtab.merge (K true)
   16.48 -
   16.49 -  fun print sg tab = ()   (*nothing extra to print*)
   16.50 -end;
   16.51 -
   16.52 -structure ConstructorsData = TheoryDataFun(ConstructorsArgs);
   16.53 -
   16.54 +  val extend = I
   16.55 +  fun merge _ tabs: T = Symtab.merge (K true) tabs;
   16.56 +  fun print _ _= ();
   16.57 +end);
   16.58  
   16.59  structure DatatypeTactics : DATATYPE_TACTICS =
   16.60  struct
   16.61  
   16.62 -fun datatype_info_sg sign name =
   16.63 -  (case Symtab.lookup (DatatypesData.get_sg sign, name) of
   16.64 +fun datatype_info thy name =
   16.65 +  (case Symtab.lookup (DatatypesData.get thy, name) of
   16.66      SOME info => info
   16.67    | NONE => error ("Unknown datatype " ^ quote name));
   16.68  
   16.69 @@ -106,11 +99,11 @@
   16.70  fun exhaust_induct_tac exh var i state =
   16.71    let
   16.72      val (_, _, Bi, _) = dest_state (state, i)
   16.73 -    val {sign, ...} = rep_thm state
   16.74 +    val thy = Thm.theory_of_thm state
   16.75      val tn = find_tname var Bi
   16.76      val rule =
   16.77 -        if exh then #exhaustion (datatype_info_sg sign tn)
   16.78 -               else #induct  (datatype_info_sg sign tn)
   16.79 +        if exh then #exhaustion (datatype_info thy tn)
   16.80 +               else #induct  (datatype_info thy tn)
   16.81      val (Const("op :",_) $ Var(ixn,_) $ _) =
   16.82          (case prems_of rule of
   16.83               [] => error "induction is not available for this datatype"
   16.84 @@ -120,7 +113,7 @@
   16.85    end
   16.86    handle Find_tname msg =>
   16.87              if exh then (*try boolean case analysis instead*)
   16.88 -		case_tac var i state
   16.89 +                case_tac var i state
   16.90              else error msg;
   16.91  
   16.92  val exhaust_tac = exhaust_induct_tac true;
   16.93 @@ -131,12 +124,10 @@
   16.94  
   16.95  fun rep_datatype_i elim induct case_eqns recursor_eqns thy =
   16.96    let
   16.97 -    val sign = sign_of thy;
   16.98 -
   16.99      (*analyze the LHS of a case equation to get a constructor*)
  16.100      fun const_of (Const("op =", _) $ (_ $ c) $ _) = c
  16.101        | const_of eqn = error ("Ill-formed case equation: " ^
  16.102 -                              Sign.string_of_term sign eqn);
  16.103 +                              Sign.string_of_term thy eqn);
  16.104  
  16.105      val constructors =
  16.106          map (head_of o const_of o FOLogic.dest_Trueprop o
  16.107 @@ -232,4 +223,3 @@
  16.108  
  16.109  val exhaust_tac = DatatypeTactics.exhaust_tac;
  16.110  val induct_tac  = DatatypeTactics.induct_tac;
  16.111 -
    17.1 --- a/src/ZF/Tools/typechk.ML	Fri Jun 17 18:33:42 2005 +0200
    17.2 +++ b/src/ZF/Tools/typechk.ML	Fri Jun 17 18:35:27 2005 +0200
    17.3 @@ -124,33 +124,26 @@
    17.4  (** global tcset **)
    17.5  
    17.6  structure TypecheckingArgs =
    17.7 -  struct
    17.8 +struct
    17.9    val name = "ZF/type-checker";
   17.10    type T = tcset ref;
   17.11    val empty = ref (TC{rules=[], net=Net.empty});
   17.12    fun copy (ref tc) = ref tc;
   17.13 -  val prep_ext = copy;
   17.14 -  fun merge (ref tc1, ref tc2) = ref (merge_tc (tc1, tc2));
   17.15 +  val extend = copy;
   17.16 +  fun merge _ (ref tc1, ref tc2) = ref (merge_tc (tc1, tc2));
   17.17    fun print _ (ref tc) = print_tc tc;
   17.18 -  end;
   17.19 +end;
   17.20  
   17.21  structure TypecheckingData = TheoryDataFun(TypecheckingArgs);
   17.22  
   17.23  val print_tcset = TypecheckingData.print;
   17.24 -val tcset_ref_of_sg = TypecheckingData.get_sg;
   17.25  val tcset_ref_of = TypecheckingData.get;
   17.26 -
   17.27 -
   17.28 -(* access global tcset *)
   17.29 +val tcset_of = ! o tcset_ref_of;
   17.30 +val tcset = tcset_of o Context.the_context;
   17.31 +val tcset_ref = tcset_ref_of o Context.the_context;
   17.32  
   17.33 -val tcset_of_sg = ! o tcset_ref_of_sg;
   17.34 -val tcset_of = tcset_of_sg o sign_of;
   17.35 -
   17.36 -val tcset = tcset_of o Context.the_context;
   17.37 -val tcset_ref = tcset_ref_of_sg o sign_of o Context.the_context;
   17.38 -
   17.39 -fun TCSET tacf st = tacf (tcset_of_sg (Thm.sign_of_thm st)) st;
   17.40 -fun TCSET' tacf i st = tacf (tcset_of_sg (Thm.sign_of_thm st)) i st;
   17.41 +fun TCSET tacf st = tacf (tcset_of (Thm.theory_of_thm st)) st;
   17.42 +fun TCSET' tacf i st = tacf (tcset_of (Thm.theory_of_thm st)) i st;
   17.43  
   17.44  
   17.45  (* change global tcset *)
   17.46 @@ -168,15 +161,14 @@
   17.47  
   17.48  (** local tcset **)
   17.49  
   17.50 -structure LocalTypecheckingArgs =
   17.51 -struct
   17.52 +structure LocalTypecheckingData = ProofDataFun
   17.53 +(struct
   17.54    val name = TypecheckingArgs.name;
   17.55    type T = tcset;
   17.56    val init = tcset_of;
   17.57    fun print _ tcset = print_tc tcset;
   17.58 -end;
   17.59 +end);
   17.60  
   17.61 -structure LocalTypecheckingData = ProofDataFun(LocalTypecheckingArgs);
   17.62  val local_tcset_of = LocalTypecheckingData.get;
   17.63  
   17.64