tuned;
authorwenzelm
Thu Apr 22 10:52:32 2004 +0200 (2004-04-22)
changeset 14643130076a81b84
parent 14642 2bfe5de2d1fa
child 14644 3224082514f9
tuned;
TFL/rules.ML
src/FOLP/simp.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/record_package.ML
src/HOLCF/IOA/meta_theory/Sequence.ML
src/HOLCF/adm.ML
src/HOLCF/domain/library.ML
src/Provers/ind.ML
src/Provers/simp.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/proof_context.ML
src/Pure/drule.ML
src/Pure/goals.ML
src/Pure/meta_simplifier.ML
src/Pure/pattern.ML
src/Pure/unify.ML
     1.1 --- a/TFL/rules.ML	Thu Apr 22 10:49:30 2004 +0200
     1.2 +++ b/TFL/rules.ML	Thu Apr 22 10:52:32 2004 +0200
     1.3 @@ -307,7 +307,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 = #tsig(Sign.rep_sg sign)
     1.8 +       val tsig = Sign.tsig_of sign
     1.9         val theta = Pattern.match tsig (P,P')
    1.10         val allI2 = instantiate (certify sign theta) allI
    1.11         val thm = Thm.implies_elim allI2 gth
    1.12 @@ -712,7 +712,7 @@
    1.13                    val mss' = MetaSimplifier.add_prems(mss, map ASSUME ants1)
    1.14                    val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') mss' Q1
    1.15                                  handle U.ERR _ => Thm.reflexive Q1
    1.16 -                  val Q2 = #2 (Logic.dest_equals (#prop(rep_thm Q1eeqQ2)))
    1.17 +                  val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2))
    1.18                    val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
    1.19                    val Q2eeqQ3 = Thm.symmetric(pbeta_reduce Q3 RS eq_reflection)
    1.20                    val thA = Thm.transitive(QeqQ1 RS eq_reflection) Q1eeqQ2
    1.21 @@ -778,7 +778,7 @@
    1.22                fun is_func (Const (name,_)) = (name = func_name)
    1.23                  | is_func _                = false
    1.24                val rcontext = rev cntxt
    1.25 -              val cncl = HOLogic.dest_Trueprop o #prop o rep_thm
    1.26 +              val cncl = HOLogic.dest_Trueprop o Thm.prop_of
    1.27                val antl = case rcontext of [] => []
    1.28                           | _   => [S.list_mk_conj(map cncl rcontext)]
    1.29                val TC = genl(S.list_mk_imp(antl, A))
     2.1 --- a/src/FOLP/simp.ML	Thu Apr 22 10:49:30 2004 +0200
     2.2 +++ b/src/FOLP/simp.ML	Thu Apr 22 10:52:32 2004 +0200
     2.3 @@ -556,7 +556,7 @@
     2.4  in find subst_thms end;
     2.5  
     2.6  fun mk_cong sg (f,aTs,rT) (refl,eq) =
     2.7 -let val tsig = #tsig(Sign.rep_sg sg);
     2.8 +let val tsig = Sign.tsig_of sg;
     2.9      val k = length aTs;
    2.10      fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) =
    2.11          let val ca = cterm_of sg va
    2.12 @@ -578,7 +578,7 @@
    2.13  
    2.14  fun mk_cong_type sg (f,T) =
    2.15  let val (aTs,rT) = strip_type T;
    2.16 -    val tsig = #tsig(Sign.rep_sg sg);
    2.17 +    val tsig = Sign.tsig_of sg;
    2.18      fun find_refl(r::rs) =
    2.19          let val (Const(eq,eqT),_,_) = dest_red(concl_of r)
    2.20          in if Type.typ_instance(tsig, rT, hd(binder_types eqT))
     3.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Apr 22 10:49:30 2004 +0200
     3.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Apr 22 10:52:32 2004 +0200
     3.3 @@ -178,7 +178,7 @@
     3.4    same type in all introduction rules*)
     3.5  fun unify_consts sign cs intr_ts =
     3.6    (let
     3.7 -    val {tsig, ...} = Sign.rep_sg sign;
     3.8 +    val tsig = Sign.tsig_of sign;
     3.9      val add_term_consts_2 =
    3.10        foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
    3.11      fun varify (t, (i, ts)) =
    3.12 @@ -264,7 +264,7 @@
    3.13  fun split_rule_var' ((t as Var (v, Type ("fun", [T1, T2])), ps), rl) =
    3.14        let val T' = prodT_factors [] ps T1 ---> T2
    3.15            val newt = ap_split [] ps T1 T2 (Var (v, T'))
    3.16 -          val cterm = Thm.cterm_of (#sign (rep_thm rl))
    3.17 +          val cterm = Thm.cterm_of (Thm.sign_of_thm rl)
    3.18        in
    3.19            instantiate ([], [(cterm t, cterm newt)]) rl
    3.20        end
    3.21 @@ -273,11 +273,11 @@
    3.22  val remove_split = rewrite_rule [split_conv RS eq_reflection];
    3.23  
    3.24  fun split_rule_vars vs rl = standard (remove_split (foldr split_rule_var'
    3.25 -  (mg_prod_factors vs ([], #prop (rep_thm rl)), rl)));
    3.26 +  (mg_prod_factors vs ([], Thm.prop_of rl), rl)));
    3.27  
    3.28  fun split_rule vs rl = standard (remove_split (foldr split_rule_var'
    3.29    (mapfilter (fn (t as Var ((a, _), _)) =>
    3.30 -    apsome (pair t) (assoc (vs, a))) (term_vars (#prop (rep_thm rl))), rl)));
    3.31 +    apsome (pair t) (assoc (vs, a))) (term_vars (Thm.prop_of rl)), rl)));
    3.32  
    3.33  
    3.34  (** process rules **)
     4.1 --- a/src/HOL/Tools/record_package.ML	Thu Apr 22 10:49:30 2004 +0200
     4.2 +++ b/src/HOL/Tools/record_package.ML	Thu Apr 22 10:52:32 2004 +0200
     4.3 @@ -107,7 +107,7 @@
     4.4  
     4.5  fun try_param_tac s rule i st =
     4.6    let
     4.7 -    val cert = cterm_of (#sign (rep_thm st));
     4.8 +    val cert = cterm_of (Thm.sign_of_thm st);
     4.9      val g = nth_elem (i - 1, prems_of st);
    4.10      val params = Logic.strip_params g;
    4.11      val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
    4.12 @@ -364,8 +364,8 @@
    4.13                               Some s => s 
    4.14                             | None => Sign.defaultS sg);
    4.15  
    4.16 -      val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm) 
    4.17 -      val {tsig,...} = Sign.rep_sg sg
    4.18 +      val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm);
    4.19 +      val tsig = Sign.tsig_of sg;
    4.20  
    4.21        fun mk_type_abbr subst name alphas = 
    4.22            let val abbrT = Type (name, map (fn a => TVar ((a,0),logicS)) alphas);
     5.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Thu Apr 22 10:49:30 2004 +0200
     5.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Thu Apr 22 10:52:32 2004 +0200
     5.3 @@ -1012,7 +1012,7 @@
     5.4  (*Generalizes over all free variables, with the named var outermost.*)
     5.5  fun all_frees_tac x i thm =
     5.6    let
     5.7 -    val tsig = #tsig (Sign.rep_sg (#sign (rep_thm thm)));
     5.8 +    val tsig = Sign.tsig_of (Thm.sign_of_thm thm);
     5.9      val frees = add_frees tsig (nth_elem (i - 1, prems_of thm), [x]);
    5.10      val frees' = sort (op >) (frees \ x) @ [x];
    5.11    in
     6.1 --- a/src/HOLCF/adm.ML	Thu Apr 22 10:49:30 2004 +0200
     6.2 +++ b/src/HOLCF/adm.ML	Thu Apr 22 10:52:32 2004 +0200
     6.3 @@ -114,7 +114,7 @@
     6.4  fun inst_adm_subst_thm state i params s T subt t paths =
     6.5    let val {sign, maxidx, ...} = rep_thm state;
     6.6        val j = maxidx+1;
     6.7 -      val {tsig, ...} = Sign.rep_sg sign;
     6.8 +      val tsig = Sign.tsig_of sign;
     6.9        val parTs = map snd (rev params);
    6.10        val rule = lift_rule (state, i) adm_subst;
    6.11        val types = the o (fst (types_sorts rule));
     7.1 --- a/src/HOLCF/domain/library.ML	Thu Apr 22 10:49:30 2004 +0200
     7.2 +++ b/src/HOLCF/domain/library.ML	Thu Apr 22 10:52:32 2004 +0200
     7.3 @@ -75,7 +75,6 @@
     7.4  
     7.5  fun rep_Type  (Type  x) = x | rep_Type  _ = Imposs "library:rep_Type";
     7.6  fun rep_TFree (TFree x) = x | rep_TFree _ = Imposs "library:rep_TFree";
     7.7 -val tsig_of = #tsig o Sign.rep_sg;
     7.8  
     7.9  fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, pcpoS);
    7.10  fun string_of_typ sg = Sign.string_of_typ sg o Sign.certify_typ sg;
     8.1 --- a/src/Provers/ind.ML	Thu Apr 22 10:49:30 2004 +0200
     8.2 +++ b/src/Provers/ind.ML	Thu Apr 22 10:52:32 2004 +0200
     8.3 @@ -41,7 +41,7 @@
     8.4  
     8.5  (*Generalizes over all free variables, with the named var outermost.*)
     8.6  fun all_frees_tac (var:string) i thm = 
     8.7 -    let val tsig = #tsig(Sign.rep_sg(#sign(rep_thm thm)));
     8.8 +    let val tsig = Sign.tsig_of (Thm.sign_of_thm thm);
     8.9          val frees = add_term_frees tsig (nth_elem(i-1,prems_of thm),[var]);
    8.10          val frees' = sort (rev_order o string_ord) (frees \ var) @ [var]
    8.11      in foldl (qnt_tac i) (all_tac,frees') thm end;
     9.1 --- a/src/Provers/simp.ML	Thu Apr 22 10:49:30 2004 +0200
     9.2 +++ b/src/Provers/simp.ML	Thu Apr 22 10:52:32 2004 +0200
     9.3 @@ -582,7 +582,7 @@
     9.4  in find subst_thms end;
     9.5  
     9.6  fun mk_cong sg (f,aTs,rT) (refl,eq) =
     9.7 -let val tsig = #tsig(Sign.rep_sg sg);
     9.8 +let val tsig = Sign.tsig_of sg;
     9.9      val k = length aTs;
    9.10      fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) =
    9.11  	let val ca = cterm_of sg va
    9.12 @@ -604,7 +604,7 @@
    9.13  
    9.14  fun mk_cong_type sg (f,T) =
    9.15  let val (aTs,rT) = strip_type T;
    9.16 -    val tsig = #tsig(Sign.rep_sg sg);
    9.17 +    val tsig = Sign.tsig_of sg;
    9.18      fun find_refl(r::rs) =
    9.19  	let val (Const(eq,eqT),_,_) = dest_red(concl_of r)
    9.20  	in if Type.typ_instance(tsig, rT, hd(binder_types eqT))
    10.1 --- a/src/Pure/Isar/locale.ML	Thu Apr 22 10:49:30 2004 +0200
    10.2 +++ b/src/Pure/Isar/locale.ML	Thu Apr 22 10:52:32 2004 +0200
    10.3 @@ -635,7 +635,8 @@
    10.4    |> Drule.implies_intr_list (Library.drop (length axs, hyps))
    10.5    |> Seq.single;
    10.6  
    10.7 -fun activate_elem _ ((ctxt, axs), Fixes fixes) = ((ctxt |> ProofContext.add_fixes fixes, axs), [])
    10.8 +fun activate_elem _ ((ctxt, axs), Fixes fixes) =
    10.9 +      ((ctxt |> ProofContext.add_fixes fixes, axs), [])
   10.10    | activate_elem _ ((ctxt, axs), Assumes asms) =
   10.11        let
   10.12          val ts = flat (map (map #1 o #2) asms);
    11.1 --- a/src/Pure/Isar/proof_context.ML	Thu Apr 22 10:49:30 2004 +0200
    11.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Apr 22 10:52:32 2004 +0200
    11.3 @@ -19,7 +19,6 @@
    11.4    val prems_of: context -> thm list
    11.5    val print_proof_data: theory -> unit
    11.6    val init: theory -> context
    11.7 -  val add_syntax: (string * typ option * mixfix option) list -> context -> context
    11.8    val is_fixed: context -> string -> bool
    11.9    val default_type: context -> string -> typ option
   11.10    val used_types: context -> string list
   11.11 @@ -105,7 +104,7 @@
   11.12    val fix: (string list * string option) list -> context -> context
   11.13    val fix_i: (string list * typ option) list -> context -> context
   11.14    val fix_direct: (string list * typ option) list -> context -> context
   11.15 -  val add_fixes: (string * typ option * mixfix option) list -> context -> context
   11.16 +  val add_fixes: (string * typ option * Syntax.mixfix option) list -> context -> context
   11.17    val fix_frees: term list -> context -> context
   11.18    val bind_skolem: context -> string list -> term -> term
   11.19    val get_case: context -> string -> string option list -> RuleCases.T
   11.20 @@ -1223,8 +1222,6 @@
   11.21  
   11.22  end;
   11.23  
   11.24 -(* CB: fix free variables occuring in ts, unless already fixed. *)
   11.25 -
   11.26  fun fix_frees ts ctxt =
   11.27    let
   11.28      val frees = foldl Term.add_frees ([], ts);
    12.1 --- a/src/Pure/drule.ML	Thu Apr 22 10:49:30 2004 +0200
    12.2 +++ b/src/Pure/drule.ML	Thu Apr 22 10:52:32 2004 +0200
    12.3 @@ -748,7 +748,7 @@
    12.4  
    12.5  (*Instantiate theorem th, reading instantiations under theory of th*)
    12.6  fun read_instantiate sinsts th =
    12.7 -    read_instantiate_sg (#sign (rep_thm th)) sinsts th;
    12.8 +    read_instantiate_sg (Thm.sign_of_thm th) sinsts th;
    12.9  
   12.10  
   12.11  (*Left-to-right replacements: tpairs = [...,(vi,ti),...].
   12.12 @@ -759,12 +759,12 @@
   12.13          and {sign=signu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu;
   12.14          val maxi = Int.max(maxidx, Int.max(maxt, maxu));
   12.15          val sign' = Sign.merge(sign, Sign.merge(signt, signu))
   12.16 -        val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) (tye, maxi) (T, U)
   12.17 +        val (tye',maxi') = Type.unify (Sign.tsig_of sign') (tye, maxi) (T, U)
   12.18            handle Type.TUNIFY => raise TYPE("Ill-typed instantiation", [T,U], [t,u])
   12.19      in  (sign', tye', maxi')  end;
   12.20  in
   12.21  fun cterm_instantiate ctpairs0 th =
   12.22 -  let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th), Vartab.empty, 0))
   12.23 +  let val (sign,tye,_) = foldr add_types (ctpairs0, (Thm.sign_of_thm th, Vartab.empty, 0))
   12.24        fun instT(ct,cu) = 
   12.25          let val inst = cterm_of sign o subst_TVars_Vartab tye o term_of
   12.26          in (inst ct, inst cu) end
    13.1 --- a/src/Pure/goals.ML	Thu Apr 22 10:49:30 2004 +0200
    13.2 +++ b/src/Pure/goals.ML	Thu Apr 22 10:52:32 2004 +0200
    13.3 @@ -707,7 +707,7 @@
    13.4  fun get_top_scope_thms thy = 
    13.5     let val sc = (get_scope_sg (Theory.sign_of thy))
    13.6     in if (null sc) then (warning "No locale in theory"; [])
    13.7 -      else map (#prop o rep_thm) (map #2 (#thms(snd(hd sc))))
    13.8 +      else map Thm.prop_of (map #2 (#thms(snd(hd sc))))
    13.9     end;
   13.10  
   13.11  fun implies_intr_some_hyps thy A_set th = 
   13.12 @@ -778,16 +778,16 @@
   13.13  		    (map (Sign.string_of_term sign) 
   13.14  		     (filter (fn x => (not (in_locale [x] sign))) 
   13.15  		      hyps)))
   13.16 -	    else if Pattern.matches (#tsig(Sign.rep_sg sign)) 
   13.17 +	    else if Pattern.matches (Sign.tsig_of sign)
   13.18  			            (Envir.beta_norm (term_of chorn), Envir.beta_norm prop)
   13.19  		 then final_th
   13.20  	    else  !result_error_fn state "proved a different theorem"
   13.21          end
   13.22    in
   13.23 -     if Sign.eq_sg(sign, #sign(rep_thm st0))
   13.24 +     if Sign.eq_sg(sign, Thm.sign_of_thm st0)
   13.25       then (prems, st0, mkresult)
   13.26       else error ("Definitions would change the proof state's signature" ^
   13.27 -		 sign_error (sign, #sign(rep_thm st0)))
   13.28 +		 sign_error (sign, Thm.sign_of_thm st0))
   13.29    end
   13.30    handle THM(s,_,_) => error("prepare_proof: exception THM was raised!\n" ^ s);
   13.31  
   13.32 @@ -994,7 +994,7 @@
   13.33  	  then warning "Warning: same as previous level"
   13.34  	  else if eq_thm_sg(th,th2) then ()
   13.35  	  else warning ("Warning: signature of proof state has changed" ^
   13.36 -		       sign_error (#sign(rep_thm th), #sign(rep_thm th2)));
   13.37 +		       sign_error (Thm.sign_of_thm th, Thm.sign_of_thm th2));
   13.38         ((th2,ths2)::(th,ths)::pairs)));
   13.39  
   13.40  fun by tac = cond_timeit (!Library.timing) 
   13.41 @@ -1096,7 +1096,7 @@
   13.42  
   13.43  (** Reading and printing terms wrt the current theory **)
   13.44  
   13.45 -fun top_sg() = #sign(rep_thm(topthm()));
   13.46 +fun top_sg() = Thm.sign_of_thm (topthm());
   13.47  
   13.48  fun read s = term_of (read_cterm (top_sg()) (s, TypeInfer.logicT));
   13.49  
    14.1 --- a/src/Pure/meta_simplifier.ML	Thu Apr 22 10:49:30 2004 +0200
    14.2 +++ b/src/Pure/meta_simplifier.ML	Thu Apr 22 10:52:32 2004 +0200
    14.3 @@ -283,7 +283,7 @@
    14.4     (exists (apl (lhs, Logic.occs)) (rhs :: prems))
    14.5    orelse
    14.6     (null prems andalso
    14.7 -    Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs))
    14.8 +    Pattern.matches (Sign.tsig_of sign) (lhs, rhs))
    14.9      (*the condition "null prems" is necessary because conditional rewrites
   14.10        with extra variables in the conditions may terminate although
   14.11        the rhs is an instance of the lhs. Example: ?m < ?n ==> f(?n) == f(?m)*)
   14.12 @@ -630,7 +630,7 @@
   14.13          val insts = if fo then Thm.cterm_first_order_match (elhs', eta_t')
   14.14                            else Thm.cterm_match (elhs', eta_t');
   14.15          val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm);
   14.16 -        val prop' = #prop (rep_thm thm');
   14.17 +        val prop' = Thm.prop_of thm';
   14.18          val unconditional = (Logic.count_prems (prop',0) = 0);
   14.19          val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
   14.20        in
   14.21 @@ -666,7 +666,7 @@
   14.22            in case opt of None => rews rrules | some => some end;
   14.23  
   14.24      fun sort_rrules rrs = let
   14.25 -      fun is_simple({thm, ...}:rrule) = case #prop (rep_thm thm) of
   14.26 +      fun is_simple({thm, ...}:rrule) = case Thm.prop_of thm of
   14.27                                        Const("==",_) $ _ $ _ => true
   14.28                                        | _                   => false
   14.29        fun sort []        (re1,re2) = re1 @ re2
   14.30 @@ -701,7 +701,7 @@
   14.31  (* conversion to apply a congruence rule to a term *)
   14.32  
   14.33  fun congc (prover,signt,maxt) {thm=cong,lhs=lhs} t =
   14.34 -  let val {sign, ...} = rep_thm cong
   14.35 +  let val sign = Thm.sign_of_thm cong
   14.36        val _ = if Sign.subsig (sign, signt) then ()
   14.37                   else error("Congruence rule from different theory")
   14.38        val rthm = if maxt = ~1 then cong else Thm.incr_indexes (maxt+1) cong;
    15.1 --- a/src/Pure/pattern.ML	Thu Apr 22 10:49:30 2004 +0200
    15.2 +++ b/src/Pure/pattern.ML	Thu Apr 22 10:52:32 2004 +0200
    15.3 @@ -287,7 +287,7 @@
    15.4              in Envir.update((F,mkabs(binders,is,u)),env') end
    15.5              handle Unif => (proj_fail params; raise Unif));
    15.6  
    15.7 -fun unify(sg,env,tus) = (sgr := sg; tsgr := #tsig(Sign.rep_sg sg);
    15.8 +fun unify(sg,env,tus) = (sgr := sg; tsgr := Sign.tsig_of sg;
    15.9                           foldl (unif []) (env,tus));
   15.10  
   15.11  
    16.1 --- a/src/Pure/unify.ML	Thu Apr 22 10:49:30 2004 +0200
    16.2 +++ b/src/Pure/unify.ML	Thu Apr 22 10:52:32 2004 +0200
    16.3 @@ -179,7 +179,7 @@
    16.4  
    16.5  fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
    16.6    if T=U then env
    16.7 -  else let val (iTs',maxidx') = Type.unify (#tsig(Sign.rep_sg (!sgr))) (iTs, maxidx) (U, T)
    16.8 +  else let val (iTs',maxidx') = Type.unify (Sign.tsig_of (!sgr)) (iTs, maxidx) (U, T)
    16.9         in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
   16.10         handle Type.TUNIFY => raise CANTUNIFY;
   16.11