refer to theory instead of low-level tsig;
authorwenzelm
Wed Aug 31 15:46:40 2005 +0200 (2005-08-31)
changeset 1720329b2563f5c11
parent 17202 d364e0fd9c2f
child 17204 6f0f8b6cd3f3
refer to theory instead of low-level tsig;
TFL/rules.ML
TFL/thry.ML
src/HOL/Extraction.thy
src/HOL/Tools/recfun_codegen.ML
src/Pure/IsaPlanner/isa_fterm.ML
src/Pure/IsaPlanner/term_lib.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/proof.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/drule.ML
src/Pure/goals.ML
src/Pure/meta_simplifier.ML
src/Pure/pattern.ML
src/Pure/proofterm.ML
src/Pure/tactic.ML
src/Pure/thm.ML
     1.1 --- a/TFL/rules.ML	Wed Aug 31 15:46:39 2005 +0200
     1.2 +++ b/TFL/rules.ML	Wed Aug 31 15:46:40 2005 +0200
     1.3 @@ -308,8 +308,7 @@
     1.4     let val gth = forall_intr v th
     1.5         val {prop=Const("all",_)$Abs(x,ty,rst),sign,...} = rep_thm gth
     1.6         val P' = Abs(x,ty, HOLogic.dest_Trueprop rst)  (* get rid of trueprop *)
     1.7 -       val tsig = Sign.tsig_of sign
     1.8 -       val theta = Pattern.match tsig (P,P')
     1.9 +       val theta = Pattern.match sign (P,P')
    1.10         val allI2 = instantiate (certify sign theta) allI
    1.11         val thm = Thm.implies_elim allI2 gth
    1.12         val {prop = tp $ (A $ Abs(_,_,M)),sign,...} = rep_thm thm
     2.1 --- a/TFL/thry.ML	Wed Aug 31 15:46:39 2005 +0200
     2.2 +++ b/TFL/thry.ML	Wed Aug 31 15:46:40 2005 +0200
     2.3 @@ -34,8 +34,7 @@
     2.4  
     2.5  fun match_term thry pat ob =
     2.6    let
     2.7 -    val tsig = Sign.tsig_of (Theory.sign_of thry)
     2.8 -    val (ty_theta, tm_theta) = Pattern.match tsig (pat,ob)
     2.9 +    val (ty_theta, tm_theta) = Pattern.match thry (pat,ob)
    2.10      fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.typ_subst_TVars ty_theta T), t)
    2.11    in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta))
    2.12    end;
    2.13 @@ -51,7 +50,7 @@
    2.14   *---------------------------------------------------------------------------*)
    2.15  
    2.16  fun typecheck thry t =
    2.17 -  Thm.cterm_of (Theory.sign_of thry) t
    2.18 +  Thm.cterm_of thry t
    2.19      handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg
    2.20        | TERM (msg, _) => raise THRY_ERR "typecheck" msg;
    2.21  
     3.1 --- a/src/HOL/Extraction.thy	Wed Aug 31 15:46:39 2005 +0200
     3.2 +++ b/src/HOL/Extraction.thy	Wed Aug 31 15:46:40 2005 +0200
     3.3 @@ -38,11 +38,11 @@
     3.4    [Extraction.add_types
     3.5        [("bool", ([], NONE)),
     3.6         ("set", ([realizes_set_proc], SOME mk_realizes_set))],
     3.7 -    Extraction.set_preprocessor (fn sg =>
     3.8 +    Extraction.set_preprocessor (fn thy =>
     3.9        Proofterm.rewrite_proof_notypes
    3.10          ([], ("HOL/elim_cong", RewriteHOLProof.elim_cong) ::
    3.11            ProofRewriteRules.rprocs true) o
    3.12 -      Proofterm.rewrite_proof (Sign.tsig_of sg)
    3.13 +      Proofterm.rewrite_proof thy
    3.14          (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o
    3.15        ProofRewriteRules.elim_vars (curry Const "arbitrary"))]
    3.16  end
     4.1 --- a/src/HOL/Tools/recfun_codegen.ML	Wed Aug 31 15:46:39 2005 +0200
     4.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Wed Aug 31 15:46:40 2005 +0200
     4.3 @@ -60,9 +60,8 @@
     4.4  fun del_redundant thy eqs [] = eqs
     4.5    | del_redundant thy eqs (eq :: eqs') =
     4.6      let
     4.7 -      val tsig = Sign.tsig_of (sign_of thy);
     4.8        val matches = curry
     4.9 -        (Pattern.matches tsig o pairself (lhs_of o fst))
    4.10 +        (Pattern.matches thy o pairself (lhs_of o fst))
    4.11      in del_redundant thy (eq :: eqs) (filter_out (matches eq) eqs') end;
    4.12  
    4.13  fun get_equations thy defs (s, T) =
     5.1 --- a/src/Pure/IsaPlanner/isa_fterm.ML	Wed Aug 31 15:46:39 2005 +0200
     5.2 +++ b/src/Pure/IsaPlanner/isa_fterm.ML	Wed Aug 31 15:46:40 2005 +0200
     5.3 @@ -31,7 +31,7 @@
     5.4      val add_upterm :
     5.5         UpTerm -> FcTerm -> FcTerm
     5.6      val clean_match_ft :
     5.7 -       Type.tsig ->
     5.8 +       theory ->
     5.9         Term.term ->
    5.10         FcTerm ->
    5.11         (
    5.12 @@ -457,9 +457,9 @@
    5.13  bound variables. New names have been introduced to make sure they are
    5.14  unique w.r.t all names in the term and each other. usednames' is
    5.15  oldnames + new names. *)
    5.16 -fun clean_match_ft tsig pat ft = 
    5.17 +fun clean_match_ft thy pat ft = 
    5.18      let val (t, (FakeTs,Ts,absterm)) = prepmatch ft in
    5.19 -      case TermLib.clean_match tsig (pat, t) of 
    5.20 +      case TermLib.clean_match thy (pat, t) of 
    5.21          NONE => NONE 
    5.22        | SOME insts => SOME (insts, FakeTs, Ts, absterm) end;
    5.23  (* ix = max var index *)
     6.1 --- a/src/Pure/IsaPlanner/term_lib.ML	Wed Aug 31 15:46:39 2005 +0200
     6.2 +++ b/src/Pure/IsaPlanner/term_lib.ML	Wed Aug 31 15:46:40 2005 +0200
     6.3 @@ -20,7 +20,7 @@
     6.4      val current_sign : unit -> Sign.sg
     6.5  
     6.6      (* Matching/unification with exceptions handled *)
     6.7 -    val clean_match : Type.tsig -> Term.term * Term.term 
     6.8 +    val clean_match : theory -> Term.term * Term.term 
     6.9                        -> ((Term.indexname * (Term.sort * Term.typ)) list 
    6.10                           * (Term.indexname * (Term.typ * Term.term)) list) option
    6.11      val clean_unify : Sign.sg -> int -> Term.term * Term.term 
    6.12 @@ -83,7 +83,7 @@
    6.13  		val has_new_vars : Term.term * Term.term -> bool
    6.14      val has_new_typ_vars : Term.term * Term.term -> bool
    6.15     (* checks to see if the lhs -> rhs is a invalid rewrite rule *)
    6.16 -    val is_not_valid_rwrule : Type.tsig -> (Term.term * Term.term) -> bool
    6.17 +    val is_not_valid_rwrule : theory -> (Term.term * Term.term) -> bool
    6.18  
    6.19      (* get the frees in a term that are of atomic type, ie non-functions *)
    6.20      val atomic_frees_of_term : Term.term -> (string * Term.typ) list
    6.21 @@ -143,8 +143,8 @@
    6.22  
    6.23  (* Higher order matching with exception handled *)
    6.24  (* returns optional instantiation *)
    6.25 -fun clean_match tsig (a as (pat, t)) = 
    6.26 -  let val (tyenv, tenv) = Pattern.match tsig a
    6.27 +fun clean_match thy (a as (pat, t)) = 
    6.28 +  let val (tyenv, tenv) = Pattern.match thy a
    6.29    in SOME (Vartab.dest tyenv, Vartab.dest tenv)
    6.30    end handle Pattern.MATCH => NONE;
    6.31  (* Higher order unification with exception handled, return the instantiations *)
    6.32 @@ -408,11 +408,11 @@
    6.33  which embeds into the rhs, this would be much closer to the normal
    6.34  notion of valid wave rule - ie there exists at least one case where it
    6.35  is a valid wave rule... *)
    6.36 -	fun is_not_valid_rwrule tysig (lhs, rhs) = 
    6.37 +	fun is_not_valid_rwrule thy (lhs, rhs) = 
    6.38        Term.is_Var (Term.head_of lhs) (* if lhs is essentially just a var *)
    6.39        orelse has_new_vars (lhs,rhs) 
    6.40        orelse has_new_typ_vars (lhs,rhs) 
    6.41 -      orelse Pattern.matches_subterm tysig (lhs, rhs);
    6.42 +      orelse Pattern.matches_subterm thy (lhs, rhs);
    6.43  
    6.44  
    6.45    (* first term contains the second in some name convertable way... *)
     7.1 --- a/src/Pure/Isar/locale.ML	Wed Aug 31 15:46:39 2005 +0200
     7.2 +++ b/src/Pure/Isar/locale.ML	Wed Aug 31 15:46:40 2005 +0200
     7.3 @@ -287,19 +287,18 @@
     7.4    fun dest regs = map (apfst untermify) (Termtab.dest regs);
     7.5  
     7.6    (* registrations that subsume t *)
     7.7 -  fun subsumers tsig t regs =
     7.8 -    List.filter (fn (t', _) => Pattern.matches tsig (t', t)) (Termtab.dest regs);
     7.9 +  fun subsumers thy t regs =
    7.10 +    List.filter (fn (t', _) => Pattern.matches thy (t', t)) (Termtab.dest regs);
    7.11  
    7.12    (* look up registration, pick one that subsumes the query *)
    7.13    fun lookup sign (regs, ts) =
    7.14      let
    7.15 -      val tsig = Sign.tsig_of sign;
    7.16        val t = termify ts;
    7.17 -      val subs = subsumers tsig t regs;
    7.18 +      val subs = subsumers sign t regs;
    7.19      in (case subs of
    7.20          [] => NONE
    7.21        | ((t', (attn, thms)) :: _) => let
    7.22 -            val (tinst, inst) = Pattern.match tsig (t', t);
    7.23 +            val (tinst, inst) = Pattern.match sign (t', t);
    7.24              (* thms contain Frees, not Vars *)
    7.25              val tinst' = tinst |> Vartab.dest
    7.26                   |> map (fn ((x, 0), (_, T)) => (x, Type.unvarifyT T))
    7.27 @@ -316,13 +315,12 @@
    7.28       additionally returns registrations that are strictly subsumed *)
    7.29    fun insert sign (ts, attn) regs =
    7.30      let
    7.31 -      val tsig = Sign.tsig_of sign;
    7.32        val t = termify ts;
    7.33 -      val subs = subsumers tsig t regs ;
    7.34 +      val subs = subsumers sign t regs ;
    7.35      in (case subs of
    7.36          [] => let
    7.37                  val sups =
    7.38 -                  List.filter (fn (t', _) => Pattern.matches tsig (t, t')) (Termtab.dest regs);
    7.39 +                  List.filter (fn (t', _) => Pattern.matches sign (t, t')) (Termtab.dest regs);
    7.40                  val sups' = map (apfst untermify) sups
    7.41                in (Termtab.update ((t, (attn, [])), regs), sups') end
    7.42        | _ => (regs, []))
     8.1 --- a/src/Pure/Isar/proof.ML	Wed Aug 31 15:46:39 2005 +0200
     8.2 +++ b/src/Pure/Isar/proof.ML	Wed Aug 31 15:46:40 2005 +0200
     8.3 @@ -490,7 +490,6 @@
     8.4            [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")]))));
     8.5  
     8.6      val {hyps, thy, ...} = Thm.rep_thm raw_th;
     8.7 -    val tsig = Sign.tsig_of thy;
     8.8      val casms = List.concat (map #1 (ProofContext.assumptions_of (context_of state)));
     8.9      val bad_hyps = Library.gen_rems Term.aconv (hyps, map Thm.term_of casms);
    8.10  
    8.11 @@ -500,7 +499,7 @@
    8.12    in
    8.13      conditional (not (null bad_hyps)) (fn () => err ("Additional hypotheses:\n" ^
    8.14          cat_lines (map (ProofContext.string_of_term ctxt) bad_hyps)));
    8.15 -    conditional (exists (not o Pattern.matches tsig) (ts ~~ map Thm.prop_of ths)) (fn () =>
    8.16 +    conditional (exists (not o Pattern.matches thy) (ts ~~ map Thm.prop_of ths)) (fn () =>
    8.17        err ("Proved a different theorem: " ^ Pretty.string_of (ProofContext.pretty_thm ctxt th)));
    8.18      ths
    8.19    end;
     9.1 --- a/src/Pure/Proof/extraction.ML	Wed Aug 31 15:46:39 2005 +0200
     9.2 +++ b/src/Pure/Proof/extraction.ML	Wed Aug 31 15:46:40 2005 +0200
     9.3 @@ -88,10 +88,8 @@
     9.4  
     9.5  fun condrew thy rules procs =
     9.6    let
     9.7 -    val tsig = Sign.tsig_of thy;
     9.8 -
     9.9      fun rew tm =
    9.10 -      Pattern.rewrite_term tsig [] (condrew' :: procs) tm
    9.11 +      Pattern.rewrite_term thy [] (condrew' :: procs) tm
    9.12      and condrew' tm =
    9.13        let
    9.14          val cache = ref ([] : (term * term) list);
    9.15 @@ -105,7 +103,7 @@
    9.16          let
    9.17            fun ren t = getOpt (Term.rename_abs tm1 tm t, t);
    9.18            val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1);
    9.19 -          val env as (Tenv, tenv) = Pattern.match tsig (inc tm1, tm);
    9.20 +          val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm);
    9.21            val prems' = map (pairself (Envir.subst_vars env o inc o ren)) prems;
    9.22            val env' = Envir.Envir
    9.23              {maxidx = Library.foldl Int.max
    9.24 @@ -321,7 +319,7 @@
    9.25      let
    9.26        val name = Thm.name_of_thm thm;
    9.27        val _ = assert (name <> "") "add_realizers: unnamed theorem";
    9.28 -      val prop = Pattern.rewrite_term (Sign.tsig_of thy')
    9.29 +      val prop = Pattern.rewrite_term thy'
    9.30          (map (Logic.dest_equals o prop_of) defs) [] (prop_of thm);
    9.31        val vars = vars_of prop;
    9.32        val vars' = filter_out (fn v =>
    9.33 @@ -350,7 +348,7 @@
    9.34        ExtractionData.get thy';
    9.35      val procs = List.concat (map (fst o snd) types);
    9.36      val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
    9.37 -    val prop' = Pattern.rewrite_term (Sign.tsig_of thy')
    9.38 +    val prop' = Pattern.rewrite_term thy'
    9.39        (map (Logic.dest_equals o prop_of) defs) [] prop;
    9.40    in freeze_thaw (condrew thy' eqns
    9.41      (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
    10.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Wed Aug 31 15:46:39 2005 +0200
    10.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Wed Aug 31 15:46:40 2005 +0200
    10.3 @@ -10,7 +10,7 @@
    10.4    val rew : bool -> typ list -> Proofterm.proof -> Proofterm.proof option
    10.5    val rprocs : bool -> (string * (typ list -> Proofterm.proof -> Proofterm.proof option)) list
    10.6    val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof
    10.7 -  val elim_defs : Sign.sg -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
    10.8 +  val elim_defs : theory -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
    10.9    val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof
   10.10  end;
   10.11  
   10.12 @@ -235,9 +235,8 @@
   10.13        | (_, []) => prf
   10.14        | (prf', ts) => proof_combt' (insert_refl defs Ts prf', ts));
   10.15  
   10.16 -fun elim_defs sign r defs prf =
   10.17 +fun elim_defs thy r defs prf =
   10.18    let
   10.19 -    val tsig = Sign.tsig_of sign;
   10.20      val defs' = map (Logic.dest_equals o prop_of o Drule.abs_def) defs
   10.21      val defnames = map Thm.name_of_thm defs;
   10.22      val f = if not r then I else
   10.23 @@ -248,9 +247,9 @@
   10.24              else map (pair s o SOME o fst) (filter_out (fn (p, _) =>
   10.25                null (term_consts p inter cnames)) ps))
   10.26            (Symtab.dest (thms_of_proof prf Symtab.empty)))
   10.27 -      in Reconstruct.expand_proof sign thms end
   10.28 +      in Reconstruct.expand_proof thy thms end
   10.29    in
   10.30 -    rewrite_terms (Pattern.rewrite_term tsig defs' [])
   10.31 +    rewrite_terms (Pattern.rewrite_term thy defs' [])
   10.32        (insert_refl defnames [] (f prf))
   10.33    end;
   10.34  
    11.1 --- a/src/Pure/drule.ML	Wed Aug 31 15:46:39 2005 +0200
    11.2 +++ b/src/Pure/drule.ML	Wed Aug 31 15:46:40 2005 +0200
    11.3 @@ -852,7 +852,7 @@
    11.4  
    11.5  fun norm_hhf thy t =
    11.6    if is_norm_hhf t then t
    11.7 -  else Pattern.rewrite_term (Sign.tsig_of thy) [Logic.dest_equals (prop_of norm_hhf_eq)] [] t;
    11.8 +  else Pattern.rewrite_term thy [Logic.dest_equals (prop_of norm_hhf_eq)] [] t;
    11.9  
   11.10  
   11.11  (*** Instantiate theorem th, reading instantiations in theory thy ****)
    12.1 --- a/src/Pure/goals.ML	Wed Aug 31 15:46:39 2005 +0200
    12.2 +++ b/src/Pure/goals.ML	Wed Aug 31 15:46:40 2005 +0200
    12.3 @@ -752,7 +752,7 @@
    12.4                      (map (Sign.string_of_term thy)
    12.5                       (List.filter (fn x => (not (in_locale [x] thy)))
    12.6                        hyps)))
    12.7 -            else if Pattern.matches (Sign.tsig_of thy)
    12.8 +            else if Pattern.matches thy
    12.9                                      (Envir.beta_norm (term_of chorn), Envir.beta_norm prop)
   12.10                   then final_th
   12.11              else  !result_error_fn state "proved a different theorem"
    13.1 --- a/src/Pure/meta_simplifier.ML	Wed Aug 31 15:46:39 2005 +0200
    13.2 +++ b/src/Pure/meta_simplifier.ML	Wed Aug 31 15:46:40 2005 +0200
    13.3 @@ -437,7 +437,7 @@
    13.4  *)
    13.5    exists (fn t => Logic.occs (lhs, t)) (rhs :: prems)
    13.6      orelse
    13.7 -  null prems andalso Pattern.matches (Sign.tsig_of thy) (lhs, rhs)
    13.8 +  null prems andalso Pattern.matches thy (lhs, rhs)
    13.9      (*the condition "null prems" is necessary because conditional rewrites
   13.10        with extra variables in the conditions may terminate although
   13.11        the rhs is an instance of the lhs; example: ?m < ?n ==> f(?n) == f(?m)*)
   13.12 @@ -796,7 +796,6 @@
   13.13      val eta_thm = Thm.eta_conversion t;
   13.14      val eta_t' = rhs_of eta_thm;
   13.15      val eta_t = term_of eta_t';
   13.16 -    val tsigt = Sign.tsig_of thyt;
   13.17      fun rew {thm, name, lhs, elhs, fo, perm} =
   13.18        let
   13.19          val {thy, prop, maxidx, ...} = rep_thm thm;
   13.20 @@ -853,7 +852,7 @@
   13.21  
   13.22      fun proc_rews [] = NONE
   13.23        | proc_rews (Proc {name, proc, lhs, ...} :: ps) =
   13.24 -          if Pattern.matches tsigt (Thm.term_of lhs, Thm.term_of t) then
   13.25 +          if Pattern.matches thyt (Thm.term_of lhs, Thm.term_of t) then
   13.26              (debug_term false ("Trying procedure " ^ quote name ^ " on:") ss thyt eta_t;
   13.27               case transform_failure (curry SIMPROC_FAIL name)
   13.28                   (fn () => proc thyt ss eta_t) () of
   13.29 @@ -1136,7 +1135,7 @@
   13.30  
   13.31  (*simple term rewriting -- no proof*)
   13.32  fun rewrite_term thy rules procs =
   13.33 -  Pattern.rewrite_term (Sign.tsig_of thy) (map decomp_simp' rules) procs;
   13.34 +  Pattern.rewrite_term thy (map decomp_simp' rules) procs;
   13.35  
   13.36  fun rewrite_thm mode prover ss = Drule.fconv_rule (rewrite_cterm mode prover ss);
   13.37  
    14.1 --- a/src/Pure/pattern.ML	Wed Aug 31 15:46:39 2005 +0200
    14.2 +++ b/src/Pure/pattern.ML	Wed Aug 31 15:46:40 2005 +0200
    14.3 @@ -15,29 +15,26 @@
    14.4  
    14.5  signature PATTERN =
    14.6  sig
    14.7 -  val trace_unify_fail  : bool ref
    14.8 -  val aeconv            : term * term -> bool
    14.9 -  val eta_contract      : term -> term
   14.10 -  val eta_long          : typ list -> term -> term
   14.11 -  val beta_eta_contract : term -> term
   14.12 -  val eta_contract_atom : term -> term
   14.13 -  val match             : Type.tsig -> term * term
   14.14 -                          -> Type.tyenv * Envir.tenv
   14.15 -  val first_order_match : Type.tsig -> term * term
   14.16 -                          -> Type.tyenv * Envir.tenv
   14.17 -  val matches           : Type.tsig -> term * term -> bool
   14.18 -  val matches_subterm   : Type.tsig -> term * term -> bool
   14.19 -  val unify             : Sign.sg * Envir.env * (term * term)list -> Envir.env
   14.20 -  val first_order       : term -> bool
   14.21 -  val pattern           : term -> bool
   14.22 -  val rewrite_term      : Type.tsig -> (term * term) list -> (term -> term option) list
   14.23 -                          -> term -> term
   14.24 +  val trace_unify_fail: bool ref
   14.25 +  val aeconv: term * term -> bool
   14.26 +  val eta_contract: term -> term
   14.27 +  val eta_long: typ list -> term -> term
   14.28 +  val beta_eta_contract: term -> term
   14.29 +  val eta_contract_atom: term -> term
   14.30 +  val match: theory -> term * term -> Type.tyenv * Envir.tenv
   14.31 +  val first_order_match: theory -> term * term -> Type.tyenv * Envir.tenv
   14.32 +  val matches: theory -> term * term -> bool
   14.33 +  val matches_subterm: theory -> term * term -> bool
   14.34 +  val unify: theory * Envir.env * (term * term)list -> Envir.env
   14.35 +  val first_order: term -> bool
   14.36 +  val pattern: term -> bool
   14.37 +  val rewrite_term: theory -> (term * term) list -> (term -> term option) list -> term -> term
   14.38    exception Unif
   14.39    exception MATCH
   14.40    exception Pattern
   14.41  end;
   14.42  
   14.43 -structure Pattern : PATTERN =
   14.44 +structure Pattern: PATTERN =
   14.45  struct
   14.46  
   14.47  exception Unif;
   14.48 @@ -45,16 +42,16 @@
   14.49  
   14.50  val trace_unify_fail = ref false;
   14.51  
   14.52 -fun string_of_term sg env binders t = Sign.string_of_term sg
   14.53 +fun string_of_term thy env binders t = Sign.string_of_term thy
   14.54    (Envir.norm_term env (subst_bounds(map Free binders,t)));
   14.55  
   14.56  fun bname binders i = fst(List.nth(binders,i));
   14.57  fun bnames binders is = space_implode " " (map (bname binders) is);
   14.58  
   14.59 -fun typ_clash sg (tye,T,U) =
   14.60 +fun typ_clash thy (tye,T,U) =
   14.61    if !trace_unify_fail
   14.62 -  then let val t = Sign.string_of_typ sg (Envir.norm_type tye T)
   14.63 -           and u = Sign.string_of_typ sg (Envir.norm_type tye U)
   14.64 +  then let val t = Sign.string_of_typ thy (Envir.norm_type tye T)
   14.65 +           and u = Sign.string_of_typ thy (Envir.norm_type tye U)
   14.66         in tracing("The following types do not unify:\n" ^ t ^ "\n" ^ u) end
   14.67    else ()
   14.68  
   14.69 @@ -72,11 +69,11 @@
   14.70    if !trace_unify_fail then clash (boundVar binders i) s
   14.71    else ()
   14.72  
   14.73 -fun proj_fail sg (env,binders,F,_,is,t) =
   14.74 +fun proj_fail thy (env,binders,F,_,is,t) =
   14.75    if !trace_unify_fail
   14.76    then let val f = Syntax.string_of_vname F
   14.77             val xs = bnames binders is
   14.78 -           val u = string_of_term sg env binders t
   14.79 +           val u = string_of_term thy env binders t
   14.80             val ys = bnames binders (loose_bnos t \\ is)
   14.81         in tracing("Cannot unify variable " ^ f ^
   14.82                 " (depending on bound variables " ^ xs ^ ")\nwith term " ^ u ^
   14.83 @@ -84,10 +81,10 @@
   14.84         end
   14.85    else ()
   14.86  
   14.87 -fun ocheck_fail sg (F,t,binders,env) =
   14.88 +fun ocheck_fail thy (F,t,binders,env) =
   14.89    if !trace_unify_fail
   14.90    then let val f = Syntax.string_of_vname F
   14.91 -           val u = string_of_term sg env binders t
   14.92 +           val u = string_of_term thy env binders t
   14.93         in tracing("Variable " ^ f ^ " occurs in term\n" ^ u ^
   14.94                    "\nCannot unify!\n")
   14.95         end
   14.96 @@ -225,29 +222,29 @@
   14.97                   end;
   14.98    in if xless(G,F) then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
   14.99  
  14.100 -fun unify_types sg (T,U, env as Envir.Envir{asol,iTs,maxidx}) =
  14.101 +fun unify_types thy (T,U, env as Envir.Envir{asol,iTs,maxidx}) =
  14.102    if T=U then env
  14.103 -  else let val (iTs',maxidx') = Sign.typ_unify sg (U, T) (iTs, maxidx)
  14.104 +  else let val (iTs',maxidx') = Sign.typ_unify thy (U, T) (iTs, maxidx)
  14.105         in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
  14.106 -       handle Type.TUNIFY => (typ_clash sg (iTs,T,U); raise Unif);
  14.107 +       handle Type.TUNIFY => (typ_clash thy (iTs,T,U); raise Unif);
  14.108  
  14.109 -fun unif sg binders (env,(s,t)) = case (Envir.head_norm env s, Envir.head_norm env t) of
  14.110 +fun unif thy binders (env,(s,t)) = case (Envir.head_norm env s, Envir.head_norm env t) of
  14.111        (Abs(ns,Ts,ts),Abs(nt,Tt,tt)) =>
  14.112           let val name = if ns = "" then nt else ns
  14.113 -         in unif sg ((name,Ts)::binders) (env,(ts,tt)) end
  14.114 -    | (Abs(ns,Ts,ts),t) => unif sg ((ns,Ts)::binders) (env,(ts,(incr t)$Bound(0)))
  14.115 -    | (t,Abs(nt,Tt,tt)) => unif sg ((nt,Tt)::binders) (env,((incr t)$Bound(0),tt))
  14.116 -    | p => cases sg (binders,env,p)
  14.117 +         in unif thy ((name,Ts)::binders) (env,(ts,tt)) end
  14.118 +    | (Abs(ns,Ts,ts),t) => unif thy ((ns,Ts)::binders) (env,(ts,(incr t)$Bound(0)))
  14.119 +    | (t,Abs(nt,Tt,tt)) => unif thy ((nt,Tt)::binders) (env,((incr t)$Bound(0),tt))
  14.120 +    | p => cases thy (binders,env,p)
  14.121  
  14.122 -and cases sg (binders,env,(s,t)) = case (strip_comb s,strip_comb t) of
  14.123 +and cases thy (binders,env,(s,t)) = case (strip_comb s,strip_comb t) of
  14.124         ((Var(F,Fty),ss),(Var(G,Gty),ts)) =>
  14.125           if F = G then flexflex1(env,binders,F,Fty,ints_of' env ss,ints_of' env ts)
  14.126                    else flexflex2(env,binders,F,Fty,ints_of' env ss,G,Gty,ints_of' env ts)
  14.127 -      | ((Var(F,Fty),ss),_)           => flexrigid sg (env,binders,F,Fty,ints_of' env ss,t)
  14.128 -      | (_,(Var(F,Fty),ts))           => flexrigid sg (env,binders,F,Fty,ints_of' env ts,s)
  14.129 -      | ((Const c,ss),(Const d,ts))   => rigidrigid sg (env,binders,c,d,ss,ts)
  14.130 -      | ((Free(f),ss),(Free(g),ts))   => rigidrigid sg (env,binders,f,g,ss,ts)
  14.131 -      | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB sg (env,binders,i,j,ss,ts)
  14.132 +      | ((Var(F,Fty),ss),_)           => flexrigid thy (env,binders,F,Fty,ints_of' env ss,t)
  14.133 +      | (_,(Var(F,Fty),ts))           => flexrigid thy (env,binders,F,Fty,ints_of' env ts,s)
  14.134 +      | ((Const c,ss),(Const d,ts))   => rigidrigid thy (env,binders,c,d,ss,ts)
  14.135 +      | ((Free(f),ss),(Free(g),ts))   => rigidrigid thy (env,binders,f,g,ss,ts)
  14.136 +      | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB thy (env,binders,i,j,ss,ts)
  14.137        | ((Abs(_),_),_)                => raise Pattern
  14.138        | (_,(Abs(_),_))                => raise Pattern
  14.139        | ((Const(c,_),_),(Free(f,_),_)) => (clash c f; raise Unif)
  14.140 @@ -258,21 +255,21 @@
  14.141        | ((Bound i,_),(Free(f,_),_))    => (clashB binders i f; raise Unif)
  14.142  
  14.143  
  14.144 -and rigidrigid sg (env,binders,(a,Ta),(b,Tb),ss,ts) =
  14.145 +and rigidrigid thy (env,binders,(a,Ta),(b,Tb),ss,ts) =
  14.146        if a<>b then (clash a b; raise Unif)
  14.147 -      else Library.foldl (unif sg binders) (unify_types sg (Ta,Tb,env), ss~~ts)
  14.148 +      else Library.foldl (unif thy binders) (unify_types thy (Ta,Tb,env), ss~~ts)
  14.149  
  14.150 -and rigidrigidB sg (env,binders,i,j,ss,ts) =
  14.151 +and rigidrigidB thy (env,binders,i,j,ss,ts) =
  14.152       if i <> j then (clashBB binders i j; raise Unif)
  14.153 -     else Library.foldl (unif sg binders) (env ,ss~~ts)
  14.154 +     else Library.foldl (unif thy binders) (env ,ss~~ts)
  14.155  
  14.156 -and flexrigid sg (params as (env,binders,F,Fty,is,t)) =
  14.157 -      if occurs(F,t,env) then (ocheck_fail sg (F,t,binders,env); raise Unif)
  14.158 +and flexrigid thy (params as (env,binders,F,Fty,is,t)) =
  14.159 +      if occurs(F,t,env) then (ocheck_fail thy (F,t,binders,env); raise Unif)
  14.160        else (let val (u,env') = proj(t,env,binders,is)
  14.161              in Envir.update (((F, Fty), mkabs (binders, is, u)), env') end
  14.162 -            handle Unif => (proj_fail sg params; raise Unif));
  14.163 +            handle Unif => (proj_fail thy params; raise Unif));
  14.164  
  14.165 -fun unify(sg,env,tus) = Library.foldl (unif sg []) (env,tus);
  14.166 +fun unify(thy,env,tus) = Library.foldl (unif thy []) (env,tus);
  14.167  
  14.168  
  14.169  (*Eta-contract a term (fully)*)
  14.170 @@ -343,38 +340,38 @@
  14.171  
  14.172  exception MATCH;
  14.173  
  14.174 -fun typ_match tsig (tyenv, TU) = Type.typ_match tsig TU tyenv
  14.175 +fun typ_match thy (tyenv, TU) = Sign.typ_match thy TU tyenv
  14.176    handle Type.TYPE_MATCH => raise MATCH;
  14.177  
  14.178  (*First-order matching;
  14.179 -  fomatch tsig (pattern, object) returns a (tyvar,typ)list and (var,term)list.
  14.180 +  fomatch thy (pattern, object) returns a (tyvar,typ)list and (var,term)list.
  14.181    The pattern and object may have variables in common.
  14.182    Instantiation does not affect the object, so matching ?a with ?a+1 works.
  14.183    Object is eta-contracted on the fly (by eta-expanding the pattern).
  14.184    Precondition: the pattern is already eta-contracted!
  14.185    Note: types are matched on the fly *)
  14.186 -fun fomatch tsig =
  14.187 +fun fomatch thy =
  14.188    let
  14.189      fun mtch (instsp as (tyinsts,insts)) = fn
  14.190          (Var(ixn,T), t)  =>
  14.191            if loose_bvar(t,0) then raise MATCH
  14.192            else (case Envir.lookup' (insts, (ixn, T)) of
  14.193 -                  NONE => (typ_match tsig (tyinsts, (T, fastype_of t)),
  14.194 +                  NONE => (typ_match thy (tyinsts, (T, fastype_of t)),
  14.195                             Vartab.update_new ((ixn, (T, t)), insts))
  14.196                  | SOME u => if t aeconv u then instsp else raise MATCH)
  14.197        | (Free (a,T), Free (b,U)) =>
  14.198 -          if a=b then (typ_match tsig (tyinsts,(T,U)), insts) else raise MATCH
  14.199 +          if a=b then (typ_match thy (tyinsts,(T,U)), insts) else raise MATCH
  14.200        | (Const (a,T), Const (b,U))  =>
  14.201 -          if a=b then (typ_match tsig (tyinsts,(T,U)), insts) else raise MATCH
  14.202 +          if a=b then (typ_match thy (tyinsts,(T,U)), insts) else raise MATCH
  14.203        | (Bound i, Bound j)  =>  if  i=j  then  instsp  else raise MATCH
  14.204        | (Abs(_,T,t), Abs(_,U,u))  =>
  14.205 -          mtch (typ_match tsig (tyinsts,(T,U)),insts) (t,u)
  14.206 +          mtch (typ_match thy (tyinsts,(T,U)),insts) (t,u)
  14.207        | (f$t, g$u) => mtch (mtch instsp (f,g)) (t, u)
  14.208        | (t, Abs(_,U,u))  =>  mtch instsp ((incr t)$(Bound 0), u)
  14.209        | _ => raise MATCH
  14.210    in mtch end;
  14.211  
  14.212 -fun first_order_match tsig = fomatch tsig (Vartab.empty, Vartab.empty);
  14.213 +fun first_order_match thy = fomatch thy (Vartab.empty, Vartab.empty);
  14.214  
  14.215  (* Matching of higher-order patterns *)
  14.216  
  14.217 @@ -389,7 +386,7 @@
  14.218            else raise MATCH
  14.219    end;
  14.220  
  14.221 -fun match tsg (po as (pat,obj)) =
  14.222 +fun match thy (po as (pat,obj)) =
  14.223  let
  14.224    (* Pre: pat and obj have same type *)
  14.225    fun mtch binders (env as (iTs,itms),(pat,obj)) =
  14.226 @@ -410,7 +407,7 @@
  14.227                Library.foldl (mtch binders) ((iTs,itms), pargs~~oargs)
  14.228          fun rigrig2((a:string,Ta),(b,Tb),oargs) =
  14.229                if a <> b then raise MATCH
  14.230 -              else rigrig1(typ_match tsg (iTs,(Ta,Tb)), oargs)
  14.231 +              else rigrig1(typ_match thy (iTs,(Ta,Tb)), oargs)
  14.232      in case ph of
  14.233           Var(ixn,T) =>
  14.234             let val is = ints_of pargs
  14.235 @@ -434,19 +431,19 @@
  14.236  
  14.237    val pT = fastype_of pat
  14.238    and oT = fastype_of obj
  14.239 -  val iTs = typ_match tsg (Vartab.empty, (pT,oT))
  14.240 +  val iTs = typ_match thy (Vartab.empty, (pT,oT))
  14.241    val insts2 = (iTs, Vartab.empty)
  14.242  
  14.243  in mtch [] (insts2, po)
  14.244 -   handle Pattern => fomatch tsg insts2 po
  14.245 +   handle Pattern => fomatch thy insts2 po
  14.246  end;
  14.247  
  14.248  (*Predicate: does the pattern match the object?*)
  14.249 -fun matches tsig po = (match tsig po; true) handle MATCH => false;
  14.250 +fun matches thy po = (match thy po; true) handle MATCH => false;
  14.251  
  14.252  (* Does pat match a subterm of obj? *)
  14.253 -fun matches_subterm tsig (pat,obj) =
  14.254 -  let fun msub(bounds,obj) = matches tsig (pat,obj) orelse
  14.255 +fun matches_subterm thy (pat,obj) =
  14.256 +  let fun msub(bounds,obj) = matches thy (pat,obj) orelse
  14.257              case obj of
  14.258                Abs(x,T,t) => let val y = variant bounds x
  14.259                                  val f = Free(":" ^ y,T)
  14.260 @@ -471,7 +468,7 @@
  14.261  
  14.262  (* rewriting -- simple but fast *)
  14.263  
  14.264 -fun rewrite_term tsig rules procs tm =
  14.265 +fun rewrite_term thy rules procs tm =
  14.266    let
  14.267      val skel0 = Bound 0;
  14.268  
  14.269 @@ -483,7 +480,7 @@
  14.270  
  14.271      fun match_rew tm (tm1, tm2) =
  14.272        let val rtm = if_none (Term.rename_abs tm1 tm tm2) tm2 in
  14.273 -        SOME (Envir.subst_vars (match tsig (tm1, tm)) rtm, rtm)
  14.274 +        SOME (Envir.subst_vars (match thy (tm1, tm)) rtm, rtm)
  14.275            handle MATCH => NONE
  14.276        end;
  14.277  
    15.1 --- a/src/Pure/proofterm.ML	Wed Aug 31 15:46:39 2005 +0200
    15.2 +++ b/src/Pure/proofterm.ML	Wed Aug 31 15:46:40 2005 +0200
    15.3 @@ -106,7 +106,7 @@
    15.4    val add_prf_rrules : (proof * proof) list -> theory -> theory
    15.5    val add_prf_rprocs : (string * (Term.typ list -> proof -> proof option)) list ->
    15.6      theory -> theory
    15.7 -  val rewrite_proof : Type.tsig -> (proof * proof) list *
    15.8 +  val rewrite_proof : theory -> (proof * proof) list *
    15.9      (string * (typ list -> proof -> proof option)) list -> proof -> proof
   15.10    val rewrite_proof_notypes : (proof * proof) list *
   15.11      (string * (typ list -> proof -> proof option)) list -> proof -> proof
   15.12 @@ -1107,8 +1107,8 @@
   15.13  
   15.14    in getOpt (rew1 [] skel0 prf, prf) end;
   15.15  
   15.16 -fun rewrite_proof tsig = rewrite_prf (fn (tyenv, f) =>
   15.17 -  Type.typ_match tsig (f ()) tyenv handle Type.TYPE_MATCH => raise PMatch);
   15.18 +fun rewrite_proof thy = rewrite_prf (fn (tyenv, f) =>
   15.19 +  Sign.typ_match thy (f ()) tyenv handle Type.TYPE_MATCH => raise PMatch);
   15.20  
   15.21  fun rewrite_proof_notypes rews = rewrite_prf fst rews;
   15.22  
    16.1 --- a/src/Pure/tactic.ML	Wed Aug 31 15:46:39 2005 +0200
    16.2 +++ b/src/Pure/tactic.ML	Wed Aug 31 15:46:40 2005 +0200
    16.3 @@ -693,7 +693,7 @@
    16.4  
    16.5      val raw_result = goal' RS Drule.rev_triv_goal;
    16.6      val prop' = prop_of raw_result;
    16.7 -    val _ = conditional (not (Pattern.matches (Sign.tsig_of thy) (prop, prop'))) (fn () =>
    16.8 +    val _ = conditional (not (Pattern.matches thy (prop, prop'))) (fn () =>
    16.9        err ("Proved a different theorem: " ^ Sign.string_of_term thy prop'));
   16.10    in
   16.11      Drule.conj_elim_precise (length props) raw_result
    17.1 --- a/src/Pure/thm.ML	Wed Aug 31 15:46:39 2005 +0200
    17.2 +++ b/src/Pure/thm.ML	Wed Aug 31 15:46:40 2005 +0200
    17.3 @@ -290,7 +290,7 @@
    17.4       ct2 as Cterm {t = t2, maxidx = maxidx2, sorts = sorts2, ...}) =
    17.5    let
    17.6      val thy_ref = merge_thys0 ct1 ct2;
    17.7 -    val (Tinsts, tinsts) = match (Sign.tsig_of (Theory.deref thy_ref)) (t1, t2);
    17.8 +    val (Tinsts, tinsts) = match (Theory.deref thy_ref) (t1, t2);
    17.9      val maxidx = Int.max (maxidx1, maxidx2);
   17.10      val sorts = Sorts.union sorts1 sorts2;
   17.11      fun mk_cTinst (ixn, (S, T)) =
   17.12 @@ -988,7 +988,7 @@
   17.13      val sorts' = Sorts.union sorts_U sorts;
   17.14    in
   17.15      (case T of TVar (v as (_, S)) =>
   17.16 -      if Type.of_sort (Sign.tsig_of thy') (U, S) then ((v, U), (thy_ref', sorts'))
   17.17 +      if Sign.of_sort thy' (U, S) then ((v, U), (thy_ref', sorts'))
   17.18        else raise TYPE ("Type not of sort " ^ Sign.string_of_sort thy' S, [U], [])
   17.19      | _ => raise TYPE (Pretty.string_of (Pretty.block
   17.20          [Pretty.str "instantiate: not a type variable",