rep_thm/cterm/ctyp: removed obsolete sign field;
authorwenzelm
Wed Apr 04 23:29:33 2007 +0200 (2007-04-04)
changeset 22596d0d2af4db18f
parent 22595 293934e41dfd
child 22597 284b2183d070
rep_thm/cterm/ctyp: removed obsolete sign field;
TFL/dcterm.ML
TFL/post.ML
TFL/rules.ML
src/FOLP/simp.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Modelcheck/MuckeSyn.ML
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/Tools/datatype_aux.ML
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/res_axioms.ML
src/HOLCF/IOA/Modelcheck/MuIOAOracle.ML
src/HOLCF/adm_tac.ML
src/Provers/Arith/fast_lin_arith.ML
src/Provers/blast.ML
src/Provers/splitter.ML
src/Pure/Proof/extraction.ML
src/Pure/codegen.ML
src/Pure/tctical.ML
src/Pure/thm.ML
src/ZF/Tools/cartprod.ML
     1.1 --- a/TFL/dcterm.ML	Wed Apr 04 20:22:32 2007 +0200
     1.2 +++ b/TFL/dcterm.ML	Wed Apr 04 23:29:33 2007 +0200
     1.3 @@ -187,9 +187,9 @@
     1.4   *---------------------------------------------------------------------------*)
     1.5  
     1.6  fun mk_prop ctm =
     1.7 -  let val {t, sign, ...} = Thm.rep_cterm ctm in
     1.8 +  let val {t, thy, ...} = Thm.rep_cterm ctm in
     1.9      if can HOLogic.dest_Trueprop t then ctm
    1.10 -    else Thm.cterm_of sign (HOLogic.mk_Trueprop t)
    1.11 +    else Thm.cterm_of thy (HOLogic.mk_Trueprop t)
    1.12    end
    1.13    handle TYPE (msg, _, _) => raise ERR "mk_prop" msg
    1.14      | TERM (msg, _) => raise ERR "mk_prop" msg;
     2.1 --- a/TFL/post.ML	Wed Apr 04 20:22:32 2007 +0200
     2.2 +++ b/TFL/post.ML	Wed Apr 04 23:29:33 2007 +0200
     2.3 @@ -105,8 +105,8 @@
     2.4  fun rewrite L = rewrite_rule (map mk_meta_eq (List.filter(not o id_thm) L))
     2.5  
     2.6  fun join_assums th =
     2.7 -  let val {sign,...} = rep_thm th
     2.8 -      val tych = cterm_of sign
     2.9 +  let val {thy,...} = rep_thm th
    2.10 +      val tych = cterm_of thy
    2.11        val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
    2.12        val cntxtl = (#1 o S.strip_imp) lhs  (* cntxtl should = cntxtr *)
    2.13        val cntxtr = (#1 o S.strip_imp) rhs  (* but union is solider *)
     3.1 --- a/TFL/rules.ML	Wed Apr 04 20:22:32 2007 +0200
     3.2 +++ b/TFL/rules.ML	Wed Apr 04 23:29:33 2007 +0200
     3.3 @@ -171,17 +171,17 @@
     3.4  (*----------------------------------------------------------------------------
     3.5   *        Disjunction
     3.6   *---------------------------------------------------------------------------*)
     3.7 -local val {prop,sign,...} = rep_thm disjI1
     3.8 +local val {prop,thy,...} = rep_thm disjI1
     3.9        val [P,Q] = term_vars prop
    3.10 -      val disj1 = Thm.forall_intr (Thm.cterm_of sign Q) disjI1
    3.11 +      val disj1 = Thm.forall_intr (Thm.cterm_of thy Q) disjI1
    3.12  in
    3.13  fun DISJ1 thm tm = thm RS (forall_elim (D.drop_prop tm) disj1)
    3.14    handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg;
    3.15  end;
    3.16  
    3.17 -local val {prop,sign,...} = rep_thm disjI2
    3.18 +local val {prop,thy,...} = rep_thm disjI2
    3.19        val [P,Q] = term_vars prop
    3.20 -      val disj2 = Thm.forall_intr (Thm.cterm_of sign P) disjI2
    3.21 +      val disj2 = Thm.forall_intr (Thm.cterm_of thy P) disjI2
    3.22  in
    3.23  fun DISJ2 tm thm = thm RS (forall_elim (D.drop_prop tm) disj2)
    3.24    handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg;
    3.25 @@ -274,14 +274,14 @@
    3.26   *        Universals
    3.27   *---------------------------------------------------------------------------*)
    3.28  local (* this is fragile *)
    3.29 -      val {prop,sign,...} = rep_thm spec
    3.30 +      val {prop,thy,...} = rep_thm spec
    3.31        val x = hd (tl (term_vars prop))
    3.32 -      val cTV = ctyp_of sign (type_of x)
    3.33 -      val gspec = forall_intr (cterm_of sign x) spec
    3.34 +      val cTV = ctyp_of thy (type_of x)
    3.35 +      val gspec = forall_intr (cterm_of thy x) spec
    3.36  in
    3.37  fun SPEC tm thm =
    3.38 -   let val {sign,T,...} = rep_cterm tm
    3.39 -       val gspec' = instantiate ([(cTV, ctyp_of sign T)], []) gspec
    3.40 +   let val {thy,T,...} = rep_cterm tm
    3.41 +       val gspec' = instantiate ([(cTV, ctyp_of thy T)], []) gspec
    3.42     in
    3.43        thm RS (forall_elim tm gspec')
    3.44     end
    3.45 @@ -293,7 +293,7 @@
    3.46  val ISPECL = fold ISPEC;
    3.47  
    3.48  (* Not optimized! Too complicated. *)
    3.49 -local val {prop,sign,...} = rep_thm allI
    3.50 +local val {prop,thy,...} = rep_thm allI
    3.51        val [P] = add_term_vars (prop, [])
    3.52        fun cty_theta s = map (fn (i, (S, ty)) => (ctyp_of s (TVar (i, S)), ctyp_of s ty))
    3.53        fun ctm_theta s = map (fn (i, (_, tm2)) =>
    3.54 @@ -306,22 +306,22 @@
    3.55  in
    3.56  fun GEN v th =
    3.57     let val gth = forall_intr v th
    3.58 -       val {prop=Const("all",_)$Abs(x,ty,rst),sign,...} = rep_thm gth
    3.59 +       val {prop=Const("all",_)$Abs(x,ty,rst),thy,...} = rep_thm gth
    3.60         val P' = Abs(x,ty, HOLogic.dest_Trueprop rst)  (* get rid of trueprop *)
    3.61 -       val theta = Pattern.match sign (P,P') (Vartab.empty, Vartab.empty);
    3.62 -       val allI2 = instantiate (certify sign theta) allI
    3.63 +       val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty);
    3.64 +       val allI2 = instantiate (certify thy theta) allI
    3.65         val thm = Thm.implies_elim allI2 gth
    3.66 -       val {prop = tp $ (A $ Abs(_,_,M)),sign,...} = rep_thm thm
    3.67 +       val {prop = tp $ (A $ Abs(_,_,M)),thy,...} = rep_thm thm
    3.68         val prop' = tp $ (A $ Abs(x,ty,M))
    3.69 -   in ALPHA thm (cterm_of sign prop')
    3.70 +   in ALPHA thm (cterm_of thy prop')
    3.71     end
    3.72  end;
    3.73  
    3.74  val GENL = fold_rev GEN;
    3.75  
    3.76  fun GEN_ALL thm =
    3.77 -   let val {prop,sign,...} = rep_thm thm
    3.78 -       val tycheck = cterm_of sign
    3.79 +   let val {prop,thy,...} = rep_thm thm
    3.80 +       val tycheck = cterm_of thy
    3.81         val vlist = map tycheck (add_term_vars (prop, []))
    3.82    in GENL vlist thm
    3.83    end;
    3.84 @@ -352,20 +352,20 @@
    3.85    let
    3.86      val lam = #2 (D.dest_comb (D.drop_prop (cconcl exth)))
    3.87      val redex = D.capply lam fvar
    3.88 -    val {sign, t = t$u,...} = Thm.rep_cterm redex
    3.89 -    val residue = Thm.cterm_of sign (Term.betapply (t, u))
    3.90 +    val {thy, t = t$u,...} = Thm.rep_cterm redex
    3.91 +    val residue = Thm.cterm_of thy (Term.betapply (t, u))
    3.92    in
    3.93      GEN fvar (DISCH residue fact) RS (exth RS Thms.choose_thm)
    3.94        handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg
    3.95    end;
    3.96  
    3.97 -local val {prop,sign,...} = rep_thm exI
    3.98 +local val {prop,thy,...} = rep_thm exI
    3.99        val [P,x] = term_vars prop
   3.100  in
   3.101  fun EXISTS (template,witness) thm =
   3.102 -   let val {prop,sign,...} = rep_thm thm
   3.103 -       val P' = cterm_of sign P
   3.104 -       val x' = cterm_of sign x
   3.105 +   let val {prop,thy,...} = rep_thm thm
   3.106 +       val P' = cterm_of thy P
   3.107 +       val x' = cterm_of thy x
   3.108         val abstr = #2 (D.dest_comb template)
   3.109     in
   3.110     thm RS (cterm_instantiate[(P',abstr), (x',witness)] exI)
   3.111 @@ -396,11 +396,11 @@
   3.112  (* Could be improved, but needs "subst_free" for certified terms *)
   3.113  
   3.114  fun IT_EXISTS blist th =
   3.115 -   let val {sign,...} = rep_thm th
   3.116 -       val tych = cterm_of sign
   3.117 +   let val {thy,...} = rep_thm th
   3.118 +       val tych = cterm_of thy
   3.119         val detype = #t o rep_cterm
   3.120         val blist' = map (fn (x,y) => (detype x, detype y)) blist
   3.121 -       fun ex v M  = cterm_of sign (S.mk_exists{Bvar=v,Body = M})
   3.122 +       fun ex v M  = cterm_of thy (S.mk_exists{Bvar=v,Body = M})
   3.123  
   3.124    in
   3.125    fold_rev (fn (b as (r1,r2)) => fn thm =>
   3.126 @@ -413,8 +413,8 @@
   3.127  (*---------------------------------------------------------------------------
   3.128   *  Faster version, that fails for some as yet unknown reason
   3.129   * fun IT_EXISTS blist th =
   3.130 - *    let val {sign,...} = rep_thm th
   3.131 - *        val tych = cterm_of sign
   3.132 + *    let val {thy,...} = rep_thm th
   3.133 + *        val tych = cterm_of thy
   3.134   *        fun detype (x,y) = ((#t o rep_cterm) x, (#t o rep_cterm) y)
   3.135   *   in
   3.136   *  fold (fn (b as (r1,r2), thm) =>
   3.137 @@ -521,8 +521,8 @@
   3.138  
   3.139  (* Note: rename_params_rule counts from 1, not 0 *)
   3.140  fun rename thm =
   3.141 -  let val {prop,sign,...} = rep_thm thm
   3.142 -      val tych = cterm_of sign
   3.143 +  let val {prop,thy,...} = rep_thm thm
   3.144 +      val tych = cterm_of thy
   3.145        val ants = Logic.strip_imp_prems prop
   3.146        val news = get (ants,1,[])
   3.147    in
   3.148 @@ -681,8 +681,8 @@
   3.149               val dummy = thm_ref := (thm :: !thm_ref)
   3.150               val dummy = ss_ref := (ss :: !ss_ref)
   3.151               (* Unquantified eliminate *)
   3.152 -             fun uq_eliminate (thm,imp,sign) =
   3.153 -                 let val tych = cterm_of sign
   3.154 +             fun uq_eliminate (thm,imp,thy) =
   3.155 +                 let val tych = cterm_of thy
   3.156                       val dummy = print_cterms "To eliminate:" [tych imp]
   3.157                       val ants = map tych (Logic.strip_imp_prems imp)
   3.158                       val eq = Logic.strip_imp_concl imp
   3.159 @@ -696,13 +696,13 @@
   3.160                    in
   3.161                    lhs_eeq_lhs2 COMP thm
   3.162                    end
   3.163 -             fun pq_eliminate (thm,sign,vlist,imp_body,lhs_eq) =
   3.164 +             fun pq_eliminate (thm,thy,vlist,imp_body,lhs_eq) =
   3.165                let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist)
   3.166                    val dummy = forall (op aconv) (ListPair.zip (vlist, args))
   3.167                      orelse error "assertion failed in CONTEXT_REWRITE_RULE"
   3.168                    val imp_body1 = subst_free (ListPair.zip (args, vstrl))
   3.169                                               imp_body
   3.170 -                  val tych = cterm_of sign
   3.171 +                  val tych = cterm_of thy
   3.172                    val ants1 = map tych (Logic.strip_imp_prems imp_body1)
   3.173                    val eq1 = Logic.strip_imp_concl imp_body1
   3.174                    val Q = get_lhs eq1
   3.175 @@ -725,13 +725,13 @@
   3.176                    val ant_th = U.itlist2 (PGEN tych) args vstrl impth1
   3.177                in ant_th COMP thm
   3.178                end
   3.179 -             fun q_eliminate (thm,imp,sign) =
   3.180 +             fun q_eliminate (thm,imp,thy) =
   3.181                let val (vlist, imp_body, used') = strip_all used imp
   3.182                    val (ants,Q) = dest_impl imp_body
   3.183                in if (pbeta_redex Q) (length vlist)
   3.184 -                 then pq_eliminate (thm,sign,vlist,imp_body,Q)
   3.185 +                 then pq_eliminate (thm,thy,vlist,imp_body,Q)
   3.186                   else
   3.187 -                 let val tych = cterm_of sign
   3.188 +                 let val tych = cterm_of thy
   3.189                       val ants1 = map tych ants
   3.190                       val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss
   3.191                       val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm
   3.192 @@ -746,11 +746,11 @@
   3.193  
   3.194               fun eliminate thm =
   3.195                 case (rep_thm thm)
   3.196 -               of {prop = (Const("==>",_) $ imp $ _), sign, ...} =>
   3.197 +               of {prop = (Const("==>",_) $ imp $ _), thy, ...} =>
   3.198                     eliminate
   3.199                      (if not(is_all imp)
   3.200 -                     then uq_eliminate (thm,imp,sign)
   3.201 -                     else q_eliminate (thm,imp,sign))
   3.202 +                     then uq_eliminate (thm,imp,thy)
   3.203 +                     else q_eliminate (thm,imp,thy))
   3.204                              (* Assume that the leading constant is ==,   *)
   3.205                  | _ => thm  (* if it is not a ==>                        *)
   3.206           in SOME(eliminate (rename thm)) end
   3.207 @@ -761,7 +761,7 @@
   3.208                val cntxt = rev(MetaSimplifier.prems_of_ss ss)
   3.209                val dummy = print_thms "cntxt:" cntxt
   3.210                val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _,
   3.211 -                   sign,...} = rep_thm thm
   3.212 +                   thy,...} = rep_thm thm
   3.213                fun genl tm = let val vlist = subtract (op aconv) globals
   3.214                                             (add_term_frees(tm,[]))
   3.215                              in fold_rev Forall vlist tm
   3.216 @@ -781,15 +781,15 @@
   3.217                val antl = case rcontext of [] => []
   3.218                           | _   => [S.list_mk_conj(map cncl rcontext)]
   3.219                val TC = genl(S.list_mk_imp(antl, A))
   3.220 -              val dummy = print_cterms "func:" [cterm_of sign func]
   3.221 +              val dummy = print_cterms "func:" [cterm_of thy func]
   3.222                val dummy = print_cterms "TC:"
   3.223 -                              [cterm_of sign (HOLogic.mk_Trueprop TC)]
   3.224 +                              [cterm_of thy (HOLogic.mk_Trueprop TC)]
   3.225                val dummy = tc_list := (TC :: !tc_list)
   3.226                val nestedp = isSome (S.find_term is_func TC)
   3.227                val dummy = if nestedp then say "nested" else say "not_nested"
   3.228                val dummy = term_ref := ([func,TC]@(!term_ref))
   3.229                val th' = if nestedp then raise RULES_ERR "solver" "nested function"
   3.230 -                        else let val cTC = cterm_of sign
   3.231 +                        else let val cTC = cterm_of thy
   3.232                                                (HOLogic.mk_Trueprop TC)
   3.233                               in case rcontext of
   3.234                                  [] => SPEC_ALL(ASSUME cTC)
     4.1 --- a/src/FOLP/simp.ML	Wed Apr 04 20:22:32 2007 +0200
     4.2 +++ b/src/FOLP/simp.ML	Wed Apr 04 23:29:33 2007 +0200
     4.3 @@ -381,12 +381,12 @@
     4.4  
     4.5  (*print lhs of conclusion of subgoal i*)
     4.6  fun pr_goal_lhs i st =
     4.7 -    writeln (Sign.string_of_term (#sign(rep_thm st)) 
     4.8 +    writeln (Sign.string_of_term (Thm.theory_of_thm st) 
     4.9               (lhs_of (prepare_goal i st)));
    4.10  
    4.11  (*print conclusion of subgoal i*)
    4.12  fun pr_goal_concl i st =
    4.13 -    writeln (Sign.string_of_term (#sign(rep_thm st)) (prepare_goal i st)) 
    4.14 +    writeln (Sign.string_of_term (Thm.theory_of_thm st) (prepare_goal i st)) 
    4.15  
    4.16  (*print subgoals i to j (inclusive)*)
    4.17  fun pr_goals (i,j) st =
    4.18 @@ -431,7 +431,7 @@
    4.19        are represented by rules, generalized over their parameters*)
    4.20  fun add_asms(ss,thm,a,anet,ats,cs) =
    4.21      let val As = strip_varify(nth_subgoal i thm, a, []);
    4.22 -        val thms = map (trivial o cterm_of(#sign(rep_thm(thm))))As;
    4.23 +        val thms = map (trivial o cterm_of(Thm.theory_of_thm thm)) As;
    4.24          val new_rws = List.concat(map mk_rew_rules thms);
    4.25          val rwrls = map mk_trans (List.concat(map mk_rew_rules thms));
    4.26          val anet' = foldr lhs_insert_thm anet rwrls
     5.1 --- a/src/HOL/Import/proof_kernel.ML	Wed Apr 04 20:22:32 2007 +0200
     5.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Apr 04 23:29:33 2007 +0200
     5.3 @@ -194,9 +194,9 @@
     5.4  
     5.5  fun simple_smart_string_of_cterm ct =
     5.6      let
     5.7 -	val {sign,t,T,...} = rep_cterm ct
     5.8 +	val {thy,t,T,...} = rep_cterm ct
     5.9  	(* Hack to avoid parse errors with Trueprop *)
    5.10 -	val ct  = (cterm_of sign (HOLogic.dest_Trueprop t)
    5.11 +	val ct  = (cterm_of thy (HOLogic.dest_Trueprop t)
    5.12  			   handle TERM _ => ct)
    5.13      in
    5.14  	quote(
    5.15 @@ -212,9 +212,9 @@
    5.16  
    5.17  fun smart_string_of_cterm ct =
    5.18      let
    5.19 -	val {sign,t,T,...} = rep_cterm ct
    5.20 +	val {thy,t,T,...} = rep_cterm ct
    5.21          (* Hack to avoid parse errors with Trueprop *)
    5.22 -	val ct  = (cterm_of sign (HOLogic.dest_Trueprop t)
    5.23 +	val ct  = (cterm_of thy (HOLogic.dest_Trueprop t)
    5.24  		   handle TERM _ => ct)
    5.25  	fun match cu = t aconv (term_of cu)
    5.26  	fun G 0 = Library.setmp show_types true (Library.setmp show_sorts true)
    5.27 @@ -225,7 +225,7 @@
    5.28  	fun F n =
    5.29  	    let
    5.30  		val str = Library.setmp show_brackets false (G n string_of_cterm) ct
    5.31 -		val cu  = read_cterm sign (str,T)
    5.32 +		val cu  = read_cterm thy (str,T)
    5.33  	    in
    5.34  		if match cu
    5.35  		then quote str
     6.1 --- a/src/HOL/Modelcheck/MuckeSyn.ML	Wed Apr 04 20:22:32 2007 +0200
     6.2 +++ b/src/HOL/Modelcheck/MuckeSyn.ML	Wed Apr 04 23:29:33 2007 +0200
     6.3 @@ -53,14 +53,14 @@
     6.4  	(fn prems => [cut_facts_tac prems 1, dtac sym 1, hyp_subst_tac 1,
     6.5  		     REPEAT (resolve_tac prems 1)]);
     6.6  
     6.7 -  val sig_move_thm = #sign (rep_thm move_thm);
     6.8 +  val sig_move_thm = Thm.theory_of_thm move_thm;
     6.9    val bCterm = cterm_of sig_move_thm (valOf (search_var "b" (concl_of move_thm)));
    6.10    val aCterm = cterm_of sig_move_thm (valOf (search_var "a" (hd(prems_of move_thm)))); 
    6.11  
    6.12  in
    6.13  
    6.14  fun move_mus i state =
    6.15 -let val sign = #sign (rep_thm state);
    6.16 +let val sign = Thm.theory_of_thm state;
    6.17      val (subgoal::_) = Library.drop(i-1,prems_of state);
    6.18      val concl = Logic.strip_imp_concl subgoal; (* recursive mu's in prems? *)
    6.19      val redex = search_mu concl;
     7.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Wed Apr 04 20:22:32 2007 +0200
     7.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Wed Apr 04 23:29:33 2007 +0200
     7.3 @@ -96,7 +96,7 @@
     7.4  in
     7.5  
     7.6  fun if_full_simp_tac sset i state =
     7.7 -let val sign = #sign (rep_thm state);
     7.8 +let val sign = Thm.theory_of_thm state;
     7.9          val (subgoal::_) = Library.drop(i-1,prems_of state);
    7.10          val prems = Logic.strip_imp_prems subgoal;
    7.11  	val concl = Logic.strip_imp_concl subgoal;
     8.1 --- a/src/HOL/Tools/datatype_aux.ML	Wed Apr 04 20:22:32 2007 +0200
     8.2 +++ b/src/HOL/Tools/datatype_aux.ML	Wed Apr 04 23:29:33 2007 +0200
     8.3 @@ -118,7 +118,7 @@
     8.4          val cong' = Thm.lift_rule (Thm.cprem_of st i) cong;
     8.5          val _ $ (_ $ (f' $ x') $ (g' $ y')) =
     8.6            Logic.strip_assums_concl (prop_of cong');
     8.7 -        val insts = map (pairself (cterm_of (#sign (rep_thm st))) o
     8.8 +        val insts = map (pairself (cterm_of (Thm.theory_of_thm st)) o
     8.9            apsnd (curry list_abs (Logic.strip_params (concl_of cong'))) o
    8.10              apfst head_of) [(f', f), (g', g), (x', x), (y', y)]
    8.11        in compose_tac (false, cterm_instantiate insts cong', 2) i st
     9.1 --- a/src/HOL/Tools/datatype_realizer.ML	Wed Apr 04 20:22:32 2007 +0200
     9.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Wed Apr 04 23:29:33 2007 +0200
     9.3 @@ -27,8 +27,8 @@
     9.4    in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
     9.5  
     9.6  fun prf_of thm =
     9.7 -  let val {sign, prop, der = (_, prf), ...} = rep_thm thm
     9.8 -  in Reconstruct.reconstruct_proof sign prop prf end;
     9.9 +  let val {thy, prop, der = (_, prf), ...} = rep_thm thm
    9.10 +  in Reconstruct.reconstruct_proof thy prop prf end;
    9.11  
    9.12  fun prf_subst_vars inst =
    9.13    Proofterm.map_proof_terms (subst_vars ([], inst)) I;
    10.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Apr 04 20:22:32 2007 +0200
    10.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Apr 04 23:29:33 2007 +0200
    10.3 @@ -356,7 +356,7 @@
    10.4  
    10.5      fun mk_funs_inv thm =
    10.6        let
    10.7 -        val {sign, prop, ...} = rep_thm thm;
    10.8 +        val {thy, prop, ...} = rep_thm thm;
    10.9          val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $
   10.10            (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop;
   10.11          val used = add_term_tfree_names (a, []);
   10.12 @@ -366,7 +366,7 @@
   10.13              val Ts = map (TFree o rpair HOLogic.typeS)
   10.14                (Name.variant_list used (replicate i "'t"));
   10.15              val f = Free ("f", Ts ---> U)
   10.16 -          in Goal.prove_global sign [] [] (Logic.mk_implies
   10.17 +          in Goal.prove_global thy [] [] (Logic.mk_implies
   10.18              (HOLogic.mk_Trueprop (HOLogic.list_all
   10.19                 (map (pair "x") Ts, S $ app_bnds f i)),
   10.20               HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
    11.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Apr 04 20:22:32 2007 +0200
    11.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Apr 04 23:29:33 2007 +0200
    11.3 @@ -64,8 +64,8 @@
    11.4  val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
    11.5  
    11.6  fun prf_of thm =
    11.7 -  let val {sign, prop, der = (_, prf), ...} = rep_thm thm
    11.8 -  in Reconstruct.expand_proof sign [("", NONE)] (Reconstruct.reconstruct_proof sign prop prf) end; (* FIXME *)
    11.9 +  let val {thy, prop, der = (_, prf), ...} = rep_thm thm
   11.10 +  in Reconstruct.expand_proof thy [("", NONE)] (Reconstruct.reconstruct_proof thy prop prf) end; (* FIXME *)
   11.11  
   11.12  fun forall_intr_prf (t, prf) =
   11.13    let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    12.1 --- a/src/HOL/Tools/record_package.ML	Wed Apr 04 20:22:32 2007 +0200
    12.2 +++ b/src/HOL/Tools/record_package.ML	Wed Apr 04 23:29:33 2007 +0200
    12.3 @@ -1703,10 +1703,10 @@
    12.4  
    12.5  fun meta_to_obj_all thm =
    12.6    let
    12.7 -    val {sign, prop, ...} = rep_thm thm;
    12.8 +    val {thy, prop, ...} = rep_thm thm;
    12.9      val params = Logic.strip_params prop;
   12.10      val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl prop);
   12.11 -    val ct = cterm_of sign
   12.12 +    val ct = cterm_of thy
   12.13        (HOLogic.mk_Trueprop (HOLogic.list_all (params, concl)));
   12.14      val thm' = Seq.hd (REPEAT (rtac allI 1) (Thm.trivial ct));
   12.15    in
    13.1 --- a/src/HOL/Tools/res_axioms.ML	Wed Apr 04 20:22:32 2007 +0200
    13.2 +++ b/src/HOL/Tools/res_axioms.ML	Wed Apr 04 23:29:33 2007 +0200
    13.3 @@ -394,10 +394,10 @@
    13.4    let val (c,rhs) = Drule.dest_equals (cprop_of (freeze_thm def))
    13.5        val (ch, frees) = c_variant_abs_multi (rhs, [])
    13.6        val (chilbert,cabs) = Thm.dest_comb ch
    13.7 -      val {sign,t, ...} = rep_cterm chilbert
    13.8 +      val {thy,t, ...} = rep_cterm chilbert
    13.9        val T = case t of Const ("Hilbert_Choice.Eps", Type("fun",[_,T])) => T
   13.10                        | _ => raise THM ("skolem_of_def: expected Eps", 0, [def])
   13.11 -      val cex = Thm.cterm_of sign (HOLogic.exists_const T)
   13.12 +      val cex = Thm.cterm_of thy (HOLogic.exists_const T)
   13.13        val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
   13.14        and conc =  c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees)));
   13.15        fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS someI_ex) 1
    14.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOAOracle.ML	Wed Apr 04 20:22:32 2007 +0200
    14.2 +++ b/src/HOLCF/IOA/Modelcheck/MuIOAOracle.ML	Wed Apr 04 23:29:33 2007 +0200
    14.3 @@ -3,9 +3,9 @@
    14.4  
    14.5  (* call_sim_tac invokes oracle "Sim" *)
    14.6  fun call_sim_tac thm_list i state = 
    14.7 -let val sign = #sign (rep_thm state);
    14.8 +let val thy = Thm.theory_of_thm state;
    14.9          val (subgoal::_) = Library.drop(i-1,prems_of state);
   14.10 -        val OraAss = sim_oracle sign (subgoal,thm_list);
   14.11 +        val OraAss = sim_oracle thy (subgoal,thm_list);
   14.12  in cut_facts_tac [OraAss] i state end;
   14.13  
   14.14  
    15.1 --- a/src/HOLCF/adm_tac.ML	Wed Apr 04 20:22:32 2007 +0200
    15.2 +++ b/src/HOLCF/adm_tac.ML	Wed Apr 04 23:29:33 2007 +0200
    15.3 @@ -110,7 +110,7 @@
    15.4  (*** instantiation of adm_subst theorem (a bit tricky) ***)
    15.5  
    15.6  fun inst_adm_subst_thm state i params s T subt t paths =
    15.7 -  let val {sign, maxidx, ...} = rep_thm state;
    15.8 +  let val {thy = sign, maxidx, ...} = rep_thm state;
    15.9        val j = maxidx+1;
   15.10        val parTs = map snd (rev params);
   15.11        val rule = Thm.lift_rule (Thm.cprem_of state i) adm_subst;
    16.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Wed Apr 04 20:22:32 2007 +0200
    16.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Apr 04 23:29:33 2007 +0200
    16.3 @@ -460,7 +460,7 @@
    16.4        fun multn2(n,thm) =
    16.5          let val SOME(mth) =
    16.6                get_first (fn th => SOME(thm RS th) handle THM _ => NONE) mult_mono_thms
    16.7 -            fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var;
    16.8 +            fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (Thm.theory_of_thm th) var;
    16.9              val cv = cvar(mth, hd(prems_of mth));
   16.10              val ct = cterm_of sg (LA_Data.number_of(n,#T(rep_cterm cv)))
   16.11          in instantiate ([],[(cv,ct)]) mth end
    17.1 --- a/src/Provers/blast.ML	Wed Apr 04 20:22:32 2007 +0200
    17.2 +++ b/src/Provers/blast.ML	Wed Apr 04 23:29:33 2007 +0200
    17.3 @@ -480,7 +480,7 @@
    17.4    Flag "upd" says that the inference updated the branch.
    17.5    Flag "dup" requests duplication of the affected formula.*)
    17.6  fun fromRule vars rl =
    17.7 -  let val trl = rl |> rep_thm |> #prop |> fromTerm |> convertRule vars
    17.8 +  let val trl = rl |> Thm.prop_of |> fromTerm |> convertRule vars
    17.9        fun tac (upd, dup,rot) i =
   17.10          emtac upd (if dup then rev_dup_elim rl else rl) i
   17.11          THEN
   17.12 @@ -512,7 +512,7 @@
   17.13    Since haz rules are now delayed, "dup" is always FALSE for
   17.14    introduction rules.*)
   17.15  fun fromIntrRule vars rl =
   17.16 -  let val trl = rl |> rep_thm |> #prop |> fromTerm |> convertIntrRule vars
   17.17 +  let val trl = rl |> Thm.prop_of |> fromTerm |> convertIntrRule vars
   17.18        fun tac (upd,dup,rot) i =
   17.19           rmtac upd (if dup then Data.dup_intr rl else rl) i
   17.20           THEN
   17.21 @@ -1248,7 +1248,7 @@
   17.22   "lim" is depth limit.*)
   17.23  fun timing_depth_tac start cs lim i st0 =
   17.24    let val st = (initialize (theory_of_thm st0); ObjectLogic.atomize_goal i st0);
   17.25 -      val {sign,...} = rep_thm st
   17.26 +      val sign = Thm.theory_of_thm st
   17.27        val skoprem = fromSubgoal (List.nth(prems_of st, i-1))
   17.28        val hyps  = strip_imp_prems skoprem
   17.29        and concl = strip_imp_concl skoprem
   17.30 @@ -1291,7 +1291,7 @@
   17.31  (*Translate subgoal i from a proof state*)
   17.32  fun trygl cs lim i =
   17.33          let val st = topthm()
   17.34 -                val {sign,...} = rep_thm st
   17.35 +                val sign = Thm.theory_of_thm st
   17.36                  val skoprem = (initialize (theory_of_thm st);
   17.37                                 fromSubgoal (List.nth(prems_of st, i-1)))
   17.38                  val hyps  = strip_imp_prems skoprem
    18.1 --- a/src/Provers/splitter.ML	Wed Apr 04 20:22:32 2007 +0200
    18.2 +++ b/src/Provers/splitter.ML	Wed Apr 04 23:29:33 2007 +0200
    18.3 @@ -293,7 +293,7 @@
    18.4  *************************************************************)
    18.5  
    18.6  fun select cmap state i =
    18.7 -  let val sg = #sign(rep_thm state)
    18.8 +  let val sg = Thm.theory_of_thm state
    18.9        val goali = nth_subgoal i state
   18.10        val Ts = rev(map #2 (Logic.strip_params goali))
   18.11        val _ $ t $ _ = Logic.strip_assums_concl goali;
   18.12 @@ -323,7 +323,7 @@
   18.13  fun inst_lift Ts t (T, U, pos) state i =
   18.14    let
   18.15      val cert = cterm_of (Thm.theory_of_thm state);
   18.16 -    val cntxt = mk_cntxt Ts t pos (T --> U) (#maxidx(rep_thm trlift));
   18.17 +    val cntxt = mk_cntxt Ts t pos (T --> U) (Thm.maxidx_of trlift);
   18.18    in cterm_instantiate [(cert P, cert cntxt)] trlift
   18.19    end;
   18.20  
   18.21 @@ -345,7 +345,7 @@
   18.22    let
   18.23      val thm' = Thm.lift_rule (Thm.cprem_of state i) thm;
   18.24      val (P, _) = strip_comb (fst (Logic.dest_equals
   18.25 -      (Logic.strip_assums_concl (#prop (rep_thm thm')))));
   18.26 +      (Logic.strip_assums_concl (Thm.prop_of thm'))));
   18.27      val cert = cterm_of (Thm.theory_of_thm state);
   18.28      val cntxt = mk_cntxt_splitthm t tt TB;
   18.29      val abss = Library.foldl (fn (t, T) => Abs ("", T, t));
    19.1 --- a/src/Pure/Proof/extraction.ML	Wed Apr 04 20:22:32 2007 +0200
    19.2 +++ b/src/Pure/Proof/extraction.ML	Wed Apr 04 23:29:33 2007 +0200
    19.3 @@ -718,12 +718,12 @@
    19.4  
    19.5      fun prep_thm (thm, vs) =
    19.6        let
    19.7 -        val {prop, der = (_, prf), sign, ...} = rep_thm thm;
    19.8 +        val {prop, der = (_, prf), thy, ...} = rep_thm thm;
    19.9          val name = Thm.get_name thm;
   19.10          val _ = name <> "" orelse error "extraction: unnamed theorem";
   19.11          val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
   19.12            quote name ^ " has no computational content")
   19.13 -      in (Reconstruct.reconstruct_proof sign prop prf, vs) end;
   19.14 +      in (Reconstruct.reconstruct_proof thy prop prf, vs) end;
   19.15  
   19.16      val defs = Library.foldl (fn (defs, (prf, vs)) =>
   19.17        fst (extr 0 defs vs [] [] [] prf)) ([], map prep_thm thms);
    20.1 --- a/src/Pure/codegen.ML	Wed Apr 04 20:22:32 2007 +0200
    20.2 +++ b/src/Pure/codegen.ML	Wed Apr 04 23:29:33 2007 +0200
    20.3 @@ -1064,8 +1064,8 @@
    20.4    Logic.mk_equals (t, eval_term thy t);
    20.5  
    20.6  fun evaluation_conv ct =
    20.7 -  let val {sign, t, ...} = rep_cterm ct
    20.8 -  in Thm.invoke_oracle_i sign "Pure.evaluation" (sign, Evaluation t) end;
    20.9 +  let val {thy, t, ...} = rep_cterm ct
   20.10 +  in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation t) end;
   20.11  
   20.12  val _ = Context.add_setup
   20.13    (Theory.add_oracle ("evaluation", evaluation_oracle));
    21.1 --- a/src/Pure/tctical.ML	Wed Apr 04 20:22:32 2007 +0200
    21.2 +++ b/src/Pure/tctical.ML	Wed Apr 04 23:29:33 2007 +0200
    21.3 @@ -422,7 +422,7 @@
    21.4  
    21.5  fun metahyps_aux_tac tacf (prem,gno) state =
    21.6    let val (insts,params,hyps,concl) = metahyps_split_prem prem 
    21.7 -      val {sign,maxidx,...} = rep_thm state
    21.8 +      val {thy = sign,maxidx,...} = rep_thm state
    21.9        val cterm = cterm_of sign
   21.10        val chyps = map cterm hyps
   21.11        val hypths = map assume chyps
   21.12 @@ -451,7 +451,7 @@
   21.13        fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
   21.14        (*A form of lifting that discharges assumptions.*)
   21.15        fun relift st =
   21.16 -        let val prop = #prop(rep_thm st)
   21.17 +        let val prop = Thm.prop_of st
   21.18              val subgoal_vars = (*Vars introduced in the subgoals*)
   21.19                    foldr add_term_vars [] (Logic.strip_imp_prems prop)
   21.20              and concl_vars = add_term_vars (Logic.strip_imp_concl prop, [])
   21.21 @@ -477,7 +477,7 @@
   21.22  fun metahyps_thms i state =
   21.23    let val prem = Logic.nth_prem (i, Thm.prop_of state) 
   21.24        val (insts,params,hyps,concl) = metahyps_split_prem prem 
   21.25 -      val cterm = cterm_of (#sign (rep_thm state))
   21.26 +      val cterm = cterm_of (Thm.theory_of_thm state)
   21.27    in SOME (map (forall_elim_vars 0 o assume o cterm) hyps) end
   21.28    handle TERM ("nth_prem", [A]) => NONE;
   21.29  
    22.1 --- a/src/Pure/thm.ML	Wed Apr 04 20:22:32 2007 +0200
    22.2 +++ b/src/Pure/thm.ML	Wed Apr 04 23:29:33 2007 +0200
    22.3 @@ -13,7 +13,6 @@
    22.4    type ctyp
    22.5    val rep_ctyp: ctyp ->
    22.6     {thy: theory,
    22.7 -    sign: theory,       (*obsolete*)
    22.8      T: typ,
    22.9      maxidx: int,
   22.10      sorts: sort list}
   22.11 @@ -27,13 +26,11 @@
   22.12    exception CTERM of string * cterm list
   22.13    val rep_cterm: cterm ->
   22.14     {thy: theory,
   22.15 -    sign: theory,       (*obsolete*)
   22.16      t: term,
   22.17      T: typ,
   22.18      maxidx: int,
   22.19      sorts: sort list}
   22.20 -  val crep_cterm: cterm ->
   22.21 -    {thy: theory, sign: theory, t: term, T: ctyp, maxidx: int, sorts: sort list}
   22.22 +  val crep_cterm: cterm -> {thy: theory, t: term, T: ctyp, maxidx: int, sorts: sort list}
   22.23    val theory_of_cterm: cterm -> theory
   22.24    val term_of: cterm -> term
   22.25    val cterm_of: theory -> term -> cterm
   22.26 @@ -54,7 +51,6 @@
   22.27    type attribute     (* = Context.generic * thm -> Context.generic * thm *)
   22.28    val rep_thm: thm ->
   22.29     {thy: theory,
   22.30 -    sign: theory,       (*obsolete*)
   22.31      der: bool * Proofterm.proof,
   22.32      tags: tag list,
   22.33      maxidx: int,
   22.34 @@ -64,7 +60,6 @@
   22.35      prop: term}
   22.36    val crep_thm: thm ->
   22.37     {thy: theory,
   22.38 -    sign: theory,       (*obsolete*)
   22.39      der: bool * Proofterm.proof,
   22.40      tags: tag list,
   22.41      maxidx: int,
   22.42 @@ -194,7 +189,7 @@
   22.43  
   22.44  fun rep_ctyp (Ctyp {thy_ref, T, maxidx, sorts}) =
   22.45    let val thy = Theory.deref thy_ref
   22.46 -  in {thy = thy, sign = thy, T = T, maxidx = maxidx, sorts = sorts} end;
   22.47 +  in {thy = thy, T = T, maxidx = maxidx, sorts = sorts} end;
   22.48  
   22.49  fun theory_of_ctyp (Ctyp {thy_ref, ...}) = Theory.deref thy_ref;
   22.50  
   22.51 @@ -233,11 +228,11 @@
   22.52  
   22.53  fun rep_cterm (Cterm {thy_ref, t, T, maxidx, sorts}) =
   22.54    let val thy =  Theory.deref thy_ref
   22.55 -  in {thy = thy, sign = thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end;
   22.56 +  in {thy = thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end;
   22.57  
   22.58  fun crep_cterm (Cterm {thy_ref, t, T, maxidx, sorts}) =
   22.59    let val thy = Theory.deref thy_ref in
   22.60 -   {thy = thy, sign = thy, t = t,
   22.61 +   {thy = thy, t = t,
   22.62        T = Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts},
   22.63      maxidx = maxidx, sorts = sorts}
   22.64    end;
   22.65 @@ -391,7 +386,7 @@
   22.66  
   22.67  fun rep_thm (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
   22.68    let val thy = Theory.deref thy_ref in
   22.69 -   {thy = thy, sign = thy, der = der, tags = tags, maxidx = maxidx,
   22.70 +   {thy = thy, der = der, tags = tags, maxidx = maxidx,
   22.71      shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}
   22.72    end;
   22.73  
   22.74 @@ -401,7 +396,7 @@
   22.75      val thy = Theory.deref thy_ref;
   22.76      fun cterm max t = Cterm {thy_ref = thy_ref, t = t, T = propT, maxidx = max, sorts = shyps};
   22.77    in
   22.78 -   {thy = thy, sign = thy, der = der, tags = tags, maxidx = maxidx, shyps = shyps,
   22.79 +   {thy = thy, der = der, tags = tags, maxidx = maxidx, shyps = shyps,
   22.80      hyps = map (cterm ~1) hyps,
   22.81      tpairs = map (pairself (cterm maxidx)) tpairs,
   22.82      prop = cterm maxidx prop}
    23.1 --- a/src/ZF/Tools/cartprod.ML	Wed Apr 04 20:22:32 2007 +0200
    23.2 +++ b/src/ZF/Tools/cartprod.ML	Wed Apr 04 23:29:33 2007 +0200
    23.3 @@ -106,7 +106,7 @@
    23.4  fun split_rule_var (Var(v,_), Type("fun",[T1,T2]), rl) =
    23.5        let val T' = factors T1 ---> T2
    23.6            val newt = ap_split T1 T2 (Var(v,T'))
    23.7 -          val cterm = Thm.cterm_of (#sign(rep_thm rl))
    23.8 +          val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
    23.9        in
   23.10            remove_split (instantiate ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)), 
   23.11                                             cterm newt)]) rl)