--- a/TFL/casesplit.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/TFL/casesplit.ML Wed Apr 04 00:11:03 2007 +0200
@@ -156,7 +156,7 @@
val (subgoalth, exp) = IsaND.fix_alls i th;
val subgoalth' = atomize_goals subgoalth;
val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1);
- val sgn = Thm.sign_of_thm th;
+ val sgn = Thm.theory_of_thm th;
val splitter_thm = mk_casesplit_goal_thm sgn fv gt;
val nsplits = Thm.nprems_of splitter_thm;
@@ -186,7 +186,7 @@
val (n,ty) = case Library.get_first getter freets
of SOME (n, ty) => (n, ty)
| _ => error ("no such variable " ^ vstr);
- val sgn = Thm.sign_of_thm th;
+ val sgn = Thm.theory_of_thm th;
val splitter_thm = mk_casesplit_goal_thm sgn (n,ty) gt;
val nsplits = Thm.nprems_of splitter_thm;
@@ -269,7 +269,7 @@
fun splitto splitths genth =
let
val _ = not (null splitths) orelse error "splitto: no given splitths";
- val sgn = Thm.sign_of_thm genth;
+ val sgn = Thm.theory_of_thm genth;
(* check if we are a member of splitths - FIXME: quicker and
more flexible with discrim net. *)
--- a/TFL/post.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/TFL/post.ML Wed Apr 04 00:11:03 2007 +0200
@@ -53,7 +53,7 @@
case termination_goals rules of
[] => error "tgoalw: no termination conditions to prove"
| L => OldGoals.goalw_cterm defs
- (Thm.cterm_of (Theory.sign_of thy)
+ (Thm.cterm_of thy
(HOLogic.mk_Trueprop(USyntax.list_mk_conj L)));
fun tgoal thy = tgoalw thy [];
@@ -240,7 +240,7 @@
val {induct, rules, tcs} =
simplify_defn strict thy cs ss congs wfs fid pats def
val rules' =
- if strict then derive_init_eqs (Theory.sign_of thy) rules eqs
+ if strict then derive_init_eqs thy rules eqs
else rules
in (thy, {rules = rules', induct = induct, tcs = tcs}) end;
--- a/TFL/tfl.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/TFL/tfl.ML Wed Apr 04 00:11:03 2007 +0200
@@ -392,7 +392,7 @@
val wfrec_R_M = map_types poly_tvars
(wfrec $ map_types poly_tvars R)
$ functional
- val def_term = mk_const_def (Theory.sign_of thy) (x, Ty, wfrec_R_M)
+ val def_term = mk_const_def thy (x, Ty, wfrec_R_M)
val ([def], thy') = PureThy.add_defs_i false [Thm.no_attributes (def_name, def_term)] thy
in (thy', def) end;
end;
@@ -502,7 +502,7 @@
val dummy =
if !trace then
writeln ("ORIGINAL PROTO_DEF: " ^
- Sign.string_of_term (Theory.sign_of thy) proto_def)
+ Sign.string_of_term thy proto_def)
else ()
val R1 = S.rand WFR
val corollary' = R.UNDISCH(R.UNDISCH WFREC_THM)
@@ -543,13 +543,12 @@
val proto_def' = subst_free[(R1,R')] proto_def
val dummy = if !trace then writeln ("proto_def' = " ^
Sign.string_of_term
- (Theory.sign_of thy) proto_def')
+ thy proto_def')
else ()
val {lhs,rhs} = S.dest_eq proto_def'
val (c,args) = S.strip_comb lhs
val (name,Ty) = dest_atom c
- val defn = mk_const_def (Theory.sign_of thy)
- (name, Ty, S.list_mk_abs (args,rhs))
+ val defn = mk_const_def thy (name, Ty, S.list_mk_abs (args,rhs))
val ([def0], theory) =
thy
|> PureThy.add_defs_i false
--- a/src/FOLP/simp.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/FOLP/simp.ML Wed Apr 04 00:11:03 2007 +0200
@@ -359,13 +359,7 @@
datatype cntrl = STOP | MK_EQ | ASMS of int | SIMP_LHS | REW | REFL | TRUE
| PROVE | POP_CS | POP_ARTR | IF;
-(*
-fun pr_cntrl c = case c of STOP => std_output("STOP") | MK_EQ => std_output("MK_EQ") |
-ASMS i => print_int i | POP_ARTR => std_output("POP_ARTR") |
-SIMP_LHS => std_output("SIMP_LHS") | REW => std_output("REW") | REFL => std_output("REFL") |
-TRUE => std_output("TRUE") | PROVE => std_output("PROVE") | POP_CS => std_output("POP_CS") | IF
-=> std_output("IF");
-*)
+
fun simp_refl([],_,ss) = ss
| simp_refl(a'::ns,a,ss) = if a'=a then simp_refl(ns,a,SIMP_LHS::REFL::ss)
else simp_refl(ns,a,ASMS(a)::SIMP_LHS::REFL::POP_ARTR::ss);
@@ -589,23 +583,21 @@
end;
fun mk_cong_thy thy f =
-let val sg = sign_of thy;
- val T = case Sign.const_type sg f of
+let val T = case Sign.const_type thy f of
NONE => error(f^" not declared") | SOME(T) => T;
val T' = Logic.incr_tvar 9 T;
-in mk_cong_type sg (Const(f,T'),T') end;
+in mk_cong_type thy (Const(f,T'),T') end;
fun mk_congs thy = List.concat o map (mk_cong_thy thy);
fun mk_typed_congs thy =
-let val sg = sign_of thy;
- val S0 = Sign.defaultS sg;
+let val S0 = Sign.defaultS thy;
fun readfT(f,s) =
- let val T = Logic.incr_tvar 9 (Sign.read_typ(sg,K(SOME(S0))) s);
- val t = case Sign.const_type sg f of
+ let val T = Logic.incr_tvar 9 (Sign.read_typ(thy, K(SOME(S0))) s);
+ val t = case Sign.const_type thy f of
SOME(_) => Const(f,T) | NONE => Free(f,T)
in (t,T) end
-in List.concat o map (mk_cong_type sg o readfT) end;
+in List.concat o map (mk_cong_type thy o readfT) end;
end (* local *)
end (* SIMP *);
--- a/src/HOL/Bali/Basis.thy Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Bali/Basis.thy Wed Apr 04 00:11:03 2007 +0200
@@ -19,7 +19,7 @@
declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *)
ML {*
-fun cond_simproc name pat pred thm = Simplifier.simproc (Thm.sign_of_thm thm) name [pat]
+fun cond_simproc name pat pred thm = Simplifier.simproc (Thm.theory_of_thm thm) name [pat]
(fn _ => fn _ => fn t => if pred t then NONE else SOME (mk_meta_eq thm));
*}
--- a/src/HOL/Import/hol4rews.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Import/hol4rews.ML Wed Apr 04 00:11:03 2007 +0200
@@ -371,7 +371,7 @@
val thy = case opt_get_output_thy thy of
"" => thy
| output_thy => if internal
- then add_hol4_cmove (Sign.full_name (sign_of thy) bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
+ then add_hol4_cmove (Sign.full_name thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
else thy
val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
val curmaps = HOL4ConstMaps.get thy
@@ -413,7 +413,7 @@
val thy = case opt_get_output_thy thy of
"" => thy
| output_thy => if internal
- then add_hol4_cmove (Sign.full_name (sign_of thy) bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
+ then add_hol4_cmove (Sign.full_name thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
else thy
val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
val curmaps = HOL4ConstMaps.get thy
@@ -437,7 +437,7 @@
fun add_hol4_pending bthy bthm hth thy =
let
- val thmname = Sign.full_name (sign_of thy) bthm
+ val thmname = Sign.full_name thy bthm
val _ = message ("Add pending " ^ bthy ^ "." ^ bthm)
val curpend = HOL4Pending.get thy
val newpend = StringPair.update_new ((bthy,bthm),hth) curpend
--- a/src/HOL/Import/import_package.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Import/import_package.ML Wed Apr 04 00:11:03 2007 +0200
@@ -39,7 +39,7 @@
fn thy =>
fn th =>
let
- val sg = sign_of_thm th
+ val sg = Thm.theory_of_thm th
val prem = hd (prems_of th)
val _ = message ("Import_tac: thyname="^thyname^", thmname="^thmname)
val _ = message ("Import trying to prove " ^ (string_of_cterm (cterm_of sg prem)))
--- a/src/HOL/Import/import_syntax.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Import/import_syntax.ML Wed Apr 04 00:11:03 2007 +0200
@@ -137,7 +137,7 @@
val thyname = get_import_thy thy
in
Library.foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol false isa thy
- | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol false isa (typ_of (read_ctyp (sign_of thy) ty)) thy) (thy,constmaps)
+ | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol false isa (typ_of (read_ctyp thy ty)) thy) (thy,constmaps)
end)
val const_moves = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
@@ -147,7 +147,7 @@
val thyname = get_import_thy thy
in
Library.foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol true isa thy
- | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol true isa (typ_of (read_ctyp (sign_of thy) ty)) thy) (thy,constmaps)
+ | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol true isa (typ_of (read_ctyp thy ty)) thy) (thy,constmaps)
end)
fun import_thy s =
--- a/src/HOL/Import/shuffler.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Import/shuffler.ML Wed Apr 04 00:11:03 2007 +0200
@@ -516,7 +516,7 @@
fun close_thm th =
let
- val thy = sign_of_thm th
+ val thy = Thm.theory_of_thm th
val c = prop_of th
val vars = add_term_frees (c,add_term_vars(c,[]))
in
--- a/src/HOL/Integ/int_arith1.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Integ/int_arith1.ML Wed Apr 04 00:11:03 2007 +0200
@@ -101,7 +101,7 @@
fun prove_conv_nohyps tacs sg = prove_conv tacs sg [];
fun prep_simproc (name, pats, proc) =
- Simplifier.simproc (Theory.sign_of (the_context())) name pats proc;
+ Simplifier.simproc (the_context()) name pats proc;
fun is_numeral (Const("Numeral.number_of", _) $ w) = true
| is_numeral _ = false
--- a/src/HOL/Integ/nat_simprocs.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML Wed Apr 04 00:11:03 2007 +0200
@@ -60,7 +60,7 @@
arith_simps @ rel_simps;
fun prep_simproc (name, pats, proc) =
- Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc;
+ Simplifier.simproc (the_context ()) name pats proc;
(*** CancelNumerals simprocs ***)
--- a/src/HOL/Integ/presburger.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Integ/presburger.ML Wed Apr 04 00:11:03 2007 +0200
@@ -281,7 +281,7 @@
fun presburger_tac q a i = ObjectLogic.atomize_tac i THEN (fn st =>
let
val g = List.nth (prems_of st, i - 1)
- val sg = sign_of_thm st
+ val sg = Thm.theory_of_thm st
(* The Abstraction step *)
val g' = if a then abstract_pres sg g else g
(* Transform the term*)
--- a/src/HOL/Library/word_setup.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Library/word_setup.ML Wed Apr 04 00:11:03 2007 +0200
@@ -35,8 +35,8 @@
then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("bs",0),Type("List.list",[Type("Word.bit",[])]))),cterm_of sg t)] fast2_th)
else NONE
| g _ _ _ = NONE
- (*lcp** val simproc1 = Simplifier.simproc (sign_of thy) "nat_to_bv" ["Word.nat_to_bv (number_of w)"] f ***)
- val simproc2 = Simplifier.simproc (sign_of thy) "bv_to_nat" ["Word.bv_to_nat (x # xs)"] g
+ (*lcp** val simproc1 = Simplifier.simproc thy "nat_to_bv" ["Word.nat_to_bv (number_of w)"] f ***)
+ val simproc2 = Simplifier.simproc thy "bv_to_nat" ["Word.bv_to_nat (x # xs)"] g
in
Simplifier.change_simpset_of thy (fn ss => ss addsimprocs [(*lcp*simproc1,**)simproc2]);
thy
--- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Wed Apr 04 00:11:03 2007 +0200
@@ -58,10 +58,9 @@
type floatfunc = float -> float
val th = theory "FloatSparseMatrix"
-val sg = sign_of th
-fun readtype s = Sign.intern_type sg s
-fun readterm s = Sign.intern_const sg s
+fun readtype s = Sign.intern_type th s
+fun readterm s = Sign.intern_const th s
val ty_list = readtype "list"
val term_Nil = readterm "Nil"
@@ -91,7 +90,7 @@
val mk_float = Float.mk_float
-fun float2cterm (a,b) = cterm_of sg (mk_float (a,b))
+fun float2cterm (a,b) = cterm_of th (mk_float (a,b))
fun approx_value_term prec f = Float.approx_float prec (fn (x, y) => (f x, f y))
@@ -99,10 +98,10 @@
let
val (flower, fupper) = approx_value_term prec pprt value
in
- (cterm_of sg flower, cterm_of sg fupper)
+ (cterm_of th flower, cterm_of th fupper)
end
-fun sign_term t = cterm_of sg t
+fun sign_term t = cterm_of th t
val empty_spvec = empty_vector_const
@@ -161,14 +160,14 @@
let
val (l, u) = approx_vector_term prec pprt vector
in
- (cterm_of sg l, cterm_of sg u)
+ (cterm_of th l, cterm_of th u)
end
fun approx_matrix prec pprt matrix =
let
val (l, u) = approx_matrix_term prec pprt matrix
in
- (cterm_of sg l, cterm_of sg u)
+ (cterm_of th l, cterm_of th u)
end
--- a/src/HOL/Nominal/nominal_package.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Wed Apr 04 00:11:03 2007 +0200
@@ -142,7 +142,7 @@
[Free (s, T)] => absfree (s, T, t2)
| _ => sys_error "indtac")
| SOME (_ $ t') => Abs ("x", fastype_of t', abstract_over (t', t2)))
- val cert = cterm_of (Thm.sign_of_thm st);
+ val cert = cterm_of (Thm.theory_of_thm st);
val Ps = map (cert o head_of o snd o getP) ts;
val indrule' = cterm_instantiate (Ps ~~
(map (cert o abstr o getP) ts')) indrule
@@ -157,7 +157,7 @@
val revcut_rl' = Thm.lift_rule cg revcut_rl;
val v = head_of (Logic.strip_assums_concl (hd (prems_of revcut_rl')));
val ps = Logic.strip_params g;
- val cert = cterm_of (sign_of_thm st);
+ val cert = cterm_of (Thm.theory_of_thm st);
in
compose_tac (false,
Thm.instantiate ([], [(cert v, cert (list_abs (ps,
@@ -244,8 +244,6 @@
Theory.add_types (map (fn (tvs, tname, mx, _) =>
(tname, length tvs, mx)) dts);
- val sign = Theory.sign_of tmp_thy;
-
val atoms = atoms_of thy;
val classes = map (NameSpace.map_base (fn s => "pt_" ^ s)) atoms;
val cp_classes = List.concat (map (fn atom1 => map (fn atom2 =>
@@ -255,7 +253,7 @@
val augment_sort_typ = map_type_tfree (fn (s, S) => TFree (s, augment_sort S));
fun prep_constr ((constrs, sorts), (cname, cargs, mx)) =
- let val (cargs', sorts') = Library.foldl (prep_typ sign) (([], sorts), cargs)
+ let val (cargs', sorts') = Library.foldl (prep_typ tmp_thy) (([], sorts), cargs)
in (constrs @ [(cname, cargs', mx)], sorts') end
fun prep_dt_spec ((dts, sorts), (tvs, tname, mx, constrs)) =
@@ -271,7 +269,7 @@
map (fn (cname, cargs, mx) => (cname, mx)) constrs) dts';
val ps = map (fn (_, n, _, _) =>
- (Sign.full_name sign n, Sign.full_name sign (n ^ "_Rep"))) dts;
+ (Sign.full_name tmp_thy n, Sign.full_name tmp_thy (n ^ "_Rep"))) dts;
val rps = map Library.swap ps;
fun replace_types (Type ("Nominal.ABS", [T, U])) =
@@ -285,7 +283,7 @@
map (augment_sort_typ o replace_types) cargs, NoSyn)) constrs)) dts';
val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
- val full_new_type_names' = map (Sign.full_name (sign_of thy)) new_type_names';
+ val full_new_type_names' = map (Sign.full_name thy) new_type_names';
val ({induction, ...},thy1) =
DatatypePackage.add_datatype_i err flat_names new_type_names' dts'' thy;
@@ -302,7 +300,7 @@
let val T = nth_dtyp i
in permT --> T --> T end) descr;
val perm_names = replicate (length new_type_names) "Nominal.perm" @
- DatatypeProp.indexify_names (map (fn i => Sign.full_name (sign_of thy1)
+ DatatypeProp.indexify_names (map (fn i => Sign.full_name thy1
("perm_" ^ name_of_typ (nth_dtyp i)))
(length new_type_names upto length descr - 1));
val perm_names_types = perm_names ~~ perm_types;
@@ -797,7 +795,7 @@
val newTs' = Library.take (length new_type_names, recTs');
val newTs = Library.take (length new_type_names, recTs);
- val full_new_type_names = map (Sign.full_name (sign_of thy)) new_type_names;
+ val full_new_type_names = map (Sign.full_name thy) new_type_names;
fun make_constr_def tname T T' ((thy, defs, eqns),
(((cname_rep, _), (cname, cargs)), (cname', mx))) =
@@ -820,8 +818,8 @@
end
val (_, l_args, r_args) = foldr constr_arg (1, [], []) cargs;
- val abs_name = Sign.intern_const (Theory.sign_of thy) ("Abs_" ^ tname);
- val rep_name = Sign.intern_const (Theory.sign_of thy) ("Rep_" ^ tname);
+ val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
+ val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
val constrT = map fastype_of l_args ---> T;
val lhs = list_comb (Const (cname, constrT), l_args);
val rhs = list_comb (Const (cname_rep, map fastype_of r_args ---> T'), r_args);
@@ -1450,7 +1448,7 @@
if length descr'' = 1 then [big_rec_name] else
map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int)
(1 upto (length descr''));
- val rec_set_names = map (Sign.full_name (Theory.sign_of thy10)) rec_set_names';
+ val rec_set_names = map (Sign.full_name thy10) rec_set_names';
val rec_fns = map (uncurry (mk_Free "f"))
(rec_fn_Ts ~~ (1 upto (length rec_fn_Ts)));
--- a/src/HOL/Nominal/nominal_permeq.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Wed Apr 04 00:11:03 2007 +0200
@@ -287,7 +287,7 @@
case Logic.strip_assums_concl (term_of goal) of
_ $ (Const ("Finite_Set.finite", _) $ (Const ("Nominal.supp", T) $ x)) =>
let
- val cert = Thm.cterm_of (sign_of_thm st);
+ val cert = Thm.cterm_of (Thm.theory_of_thm st);
val ps = Logic.strip_params (term_of goal);
val Ts = rev (map snd ps);
val vs = collect_vars 0 x [];
@@ -327,7 +327,7 @@
case Logic.strip_assums_concl (term_of goal) of
_ $ (Const ("Nominal.fresh", Type ("fun", [T, _])) $ _ $ t) =>
let
- val cert = Thm.cterm_of (sign_of_thm st);
+ val cert = Thm.cterm_of (Thm.theory_of_thm st);
val ps = Logic.strip_params (term_of goal);
val Ts = rev (map snd ps);
val vs = collect_vars 0 t [];
--- a/src/HOL/Real/ferrante_rackoff.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Real/ferrante_rackoff.ML Wed Apr 04 00:11:03 2007 +0200
@@ -76,7 +76,7 @@
THEN (fn st =>
let
val g = nth (prems_of st) (i - 1)
- val thy = sign_of_thm st
+ val thy = Thm.theory_of_thm st
(* Transform the term*)
val (t,np,nh) = prepare_for_linr q g
(* Some simpsets for dealing with mod div abs and nat*)
--- a/src/HOL/Real/float.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Real/float.ML Wed Apr 04 00:11:03 2007 +0200
@@ -424,7 +424,7 @@
fun invoke_float_op c =
let
val th = (if length(!th) = 0 then th := [theory "MatrixLP"] else (); hd (!th))
- val sg = (if length(!sg) = 0 then sg := [sign_of th] else (); hd (!sg))
+ val sg = (if length(!sg) = 0 then sg := [th] else (); hd (!sg))
in
invoke_oracle th "float_op" (sg, Float_op_oracle_data c)
end
@@ -463,7 +463,7 @@
fun invoke_nat_op c =
let
val th = (if length (!th) = 0 then th := [theory "MatrixLP"] else (); hd (!th))
- val sg = (if length (!sg) = 0 then sg := [sign_of th] else (); hd (!sg))
+ val sg = (if length (!sg) = 0 then sg := [th] else (); hd (!sg))
in
invoke_oracle th "nat_op" (sg, Nat_op_oracle_data c)
end
--- a/src/HOL/Tools/Presburger/presburger.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML Wed Apr 04 00:11:03 2007 +0200
@@ -281,7 +281,7 @@
fun presburger_tac q a i = ObjectLogic.atomize_tac i THEN (fn st =>
let
val g = List.nth (prems_of st, i - 1)
- val sg = sign_of_thm st
+ val sg = Thm.theory_of_thm st
(* The Abstraction step *)
val g' = if a then abstract_pres sg g else g
(* Transform the term*)
--- a/src/HOL/Tools/datatype_abs_proofs.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Wed Apr 04 00:11:03 2007 +0200
@@ -112,7 +112,7 @@
if length descr' = 1 then [big_rec_name'] else
map ((curry (op ^) (big_rec_name' ^ "_")) o string_of_int)
(1 upto (length descr'));
- val rec_set_names = map (Sign.full_name (Theory.sign_of thy0)) rec_set_names';
+ val rec_set_names = map (Sign.full_name thy0) rec_set_names';
val (rec_result_Ts, reccomb_fn_Ts) = DatatypeProp.make_primrec_Ts descr sorts used;
@@ -228,7 +228,7 @@
(* define primrec combinators *)
val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
- val reccomb_names = map (Sign.full_name (Theory.sign_of thy1))
+ val reccomb_names = map (Sign.full_name thy1)
(if length descr' = 1 then [big_reccomb_name] else
(map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
(1 upto (length descr'))));
@@ -294,8 +294,7 @@
in Const ("arbitrary", Ts @ Ts' ---> T')
end) constrs) descr';
- val case_names = map (fn s =>
- Sign.full_name (Theory.sign_of thy1) (s ^ "_case")) new_type_names;
+ val case_names = map (fn s => Sign.full_name thy1 (s ^ "_case")) new_type_names;
(* define case combinators via primrec combinators *)
@@ -402,7 +401,7 @@
val size_name = "Nat.size";
val size_names = replicate (length (hd descr)) size_name @
- map (Sign.full_name (Theory.sign_of thy1)) (DatatypeProp.indexify_names
+ map (Sign.full_name thy1) (DatatypeProp.indexify_names
(map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs))));
val def_names = map (fn s => s ^ "_def") (DatatypeProp.indexify_names
(map (fn T => name_of_typ T ^ "_size") recTs));
@@ -499,7 +498,7 @@
let
val (Const ("==>", _) $ tm $ _) = t;
val (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ Ma)) = tm;
- val cert = cterm_of (Theory.sign_of thy);
+ val cert = cterm_of thy;
val nchotomy' = nchotomy RS spec;
val nchotomy'' = cterm_instantiate
[(cert (hd (add_term_vars (concl_of nchotomy', []))), cert Ma)] nchotomy'
--- a/src/HOL/Tools/datatype_aux.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Tools/datatype_aux.ML Wed Apr 04 00:11:03 2007 +0200
@@ -139,7 +139,7 @@
NONE => let val [Free (s, T)] = add_term_frees (t2, [])
in absfree (s, T, t2) end
| SOME (_ $ t') => Abs ("x", fastype_of t', abstract_over (t', t2)))
- val cert = cterm_of (Thm.sign_of_thm st);
+ val cert = cterm_of (Thm.theory_of_thm st);
val Ps = map (cert o head_of o snd o getP) ts;
val indrule' = cterm_instantiate (Ps ~~
(map (cert o abstr o getP) ts')) indrule
@@ -151,7 +151,7 @@
fun exh_tac exh_thm_of i state =
let
- val thy = Thm.sign_of_thm state;
+ val thy = Thm.theory_of_thm state;
val prem = nth (prems_of state) (i - 1);
val params = Logic.strip_params prem;
val (_, Type (tname, _)) = hd (rev params);
--- a/src/HOL/Tools/datatype_codegen.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML Wed Apr 04 00:11:03 2007 +0200
@@ -65,7 +65,6 @@
fun add_dt_defs thy defs dep module gr (descr: DatatypeAux.descr) =
let
- val sg = sign_of thy;
val tab = DatatypePackage.get_datatypes thy;
val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr;
--- a/src/HOL/Tools/datatype_package.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Tools/datatype_package.ML Wed Apr 04 00:11:03 2007 +0200
@@ -150,7 +150,7 @@
fun infer_tname state i aterm =
let
- val sign = Thm.sign_of_thm state;
+ val sign = Thm.theory_of_thm state;
val (_, _, Bi, _) = Thm.dest_state (state, i)
val params = Logic.strip_params Bi; (*params of subgoal i*)
val params = rev (rename_wrt_term Bi params); (*as they are printed*)
@@ -229,7 +229,7 @@
let val tn = infer_tname state i t in
if tn = HOLogic.boolN then inst_tac [(("P", 0), t)] case_split_thm i state
else case_inst_tac inst_tac t
- (#exhaustion (the_datatype (Thm.sign_of_thm state) tn))
+ (#exhaustion (the_datatype (Thm.theory_of_thm state) tn))
i state
end handle THM _ => Seq.empty;
--- a/src/HOL/Tools/datatype_prop.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Tools/datatype_prop.ML Wed Apr 04 00:11:03 2007 +0200
@@ -177,8 +177,6 @@
fun make_primrecs new_type_names descr sorts thy =
let
- val sign = Theory.sign_of thy;
-
val descr' = List.concat descr;
val recTs = get_rec_types descr' sorts;
val used = foldr add_typ_tfree_names [] recTs;
@@ -189,7 +187,7 @@
(reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
- val reccomb_names = map (Sign.intern_const sign)
+ val reccomb_names = map (Sign.intern_const thy)
(if length descr' = 1 then [big_reccomb_name] else
(map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
(1 upto (length descr'))));
@@ -241,7 +239,7 @@
in Ts ---> T' end) constrs) (hd descr);
val case_names = map (fn s =>
- Sign.intern_const (Theory.sign_of thy) (s ^ "_case")) new_type_names
+ Sign.intern_const thy (s ^ "_case")) new_type_names
in
map (fn ((name, Ts), T) => list_comb
(Const (name, Ts @ [T] ---> T'),
@@ -360,7 +358,7 @@
val size_name = "Nat.size";
val size_names = replicate (length (hd descr)) size_name @
- map (Sign.intern_const (Theory.sign_of thy)) (indexify_names
+ map (Sign.intern_const thy) (indexify_names
(map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs))));
val size_consts = map (fn (s, T) =>
Const (s, T --> HOLogic.natT)) (size_names ~~ recTs);
--- a/src/HOL/Tools/datatype_realizer.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Wed Apr 04 00:11:03 2007 +0200
@@ -42,7 +42,6 @@
fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : datatype_info) (is, thy) =
let
- val sg = sign_of thy;
val recTs = get_rec_types descr sorts;
val pnames = if length descr = 1 then ["P"]
else map (fn i => "P" ^ string_of_int i) (1 upto length descr);
@@ -115,7 +114,7 @@
(map (fn ((((i, _), T), U), tname) =>
make_pred i U T (mk_proj i is r) (Free (tname, T)))
(descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
- val cert = cterm_of sg;
+ val cert = cterm_of thy;
val inst = map (pairself cert) (map head_of (HOLogic.dest_conj
(HOLogic.dest_Trueprop (concl_of induction))) ~~ ps);
--- a/src/HOL/Tools/datatype_rep_proofs.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Wed Apr 04 00:11:03 2007 +0200
@@ -71,7 +71,7 @@
(if length descr' = 1 then [big_rec_name] else
(map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int)
(1 upto (length descr'))));
- val rep_set_names = map (Sign.full_name (Theory.sign_of thy1)) rep_set_names';
+ val rep_set_names = map (Sign.full_name thy1) rep_set_names';
val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
val leafTs' = get_nonrec_types descr' sorts;
@@ -200,8 +200,8 @@
val rep_names = map (curry op ^ "Rep_") new_type_names;
val rep_names' = map (fn i => big_rep_name ^ (string_of_int i))
(1 upto (length (List.concat (tl descr))));
- val all_rep_names = map (Sign.intern_const (Theory.sign_of thy3)) rep_names @
- map (Sign.full_name (Theory.sign_of thy3)) rep_names';
+ val all_rep_names = map (Sign.intern_const thy3) rep_names @
+ map (Sign.full_name thy3) rep_names';
(* isomorphism declarations *)
@@ -224,8 +224,8 @@
val (_, l_args, r_args) = foldr constr_arg (1, [], []) cargs;
val constrT = (map (typ_of_dtyp descr' sorts) cargs) ---> T;
- val abs_name = Sign.intern_const (Theory.sign_of thy) ("Abs_" ^ tname);
- val rep_name = Sign.intern_const (Theory.sign_of thy) ("Rep_" ^ tname);
+ val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
+ val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
val lhs = list_comb (Const (cname, constrT), l_args);
val rhs = mk_univ_inj r_args n i;
val def = equals T $ lhs $ (Const (abs_name, Univ_elT --> T) $ rhs);
@@ -245,11 +245,10 @@
((((_, (_, _, constrs)), tname), T), constr_syntax)) =
let
val _ $ (_ $ (cong_f $ _) $ _) = concl_of arg_cong;
- val sg = Theory.sign_of thy;
- val rep_const = cterm_of sg
- (Const (Sign.intern_const sg ("Rep_" ^ tname), T --> Univ_elT));
- val cong' = standard (cterm_instantiate [(cterm_of sg cong_f, rep_const)] arg_cong);
- val dist = standard (cterm_instantiate [(cterm_of sg distinct_f, rep_const)] distinct_lemma);
+ val rep_const = cterm_of thy
+ (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> Univ_elT));
+ val cong' = standard (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong);
+ val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
val (thy', defs', eqns', _) = Library.foldl ((make_constr_def tname T) (length constrs))
((add_path flat_names tname thy, defs, [], 1), constrs ~~ constr_syntax)
in
@@ -570,7 +569,7 @@
mk_Free "x" T i;
val Abs_t = if i < length newTs then
- Const (Sign.intern_const (Theory.sign_of thy6)
+ Const (Sign.intern_const thy6
("Abs_" ^ (List.nth (new_type_names, i))), Univ_elT --> T)
else Const ("Inductive.myinv", [T --> Univ_elT, Univ_elT] ---> T) $
Const (List.nth (all_rep_names, i), T --> Univ_elT)
@@ -584,7 +583,7 @@
val (indrule_lemma_prems, indrule_lemma_concls) =
Library.foldl mk_indrule_lemma (([], []), (descr' ~~ recTs));
- val cert = cterm_of (Theory.sign_of thy6);
+ val cert = cterm_of thy6;
val indrule_lemma = Goal.prove_global thy6 [] []
(Logic.mk_implies
--- a/src/HOL/Tools/record_package.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Tools/record_package.ML Wed Apr 04 00:11:03 2007 +0200
@@ -481,7 +481,6 @@
fun add_parents thy NONE parents = parents
| add_parents thy (SOME (types, name)) parents =
let
- val sign = Theory.sign_of thy;
fun err msg = error (msg ^ " parent record " ^ quote name);
val {args, parent, fields, extension, induct} =
@@ -489,7 +488,7 @@
val _ = if length types <> length args then err "Bad number of arguments for" else ();
fun bad_inst ((x, S), T) =
- if Sign.of_sort sign (T, S) then NONE else SOME x
+ if Sign.of_sort thy (T, S) then NONE else SOME x
val bads = List.mapPartial bad_inst (args ~~ types);
val _ = null bads orelse err ("Ill-sorted instantiation of " ^ commas bads ^ " in");
@@ -1720,11 +1719,9 @@
fun record_definition (args, bname) parent (parents: parent_info list) raw_fields thy =
(* smlnj needs type annotation of parents *)
let
- val sign = Theory.sign_of thy;
-
val alphas = map fst args;
- val name = Sign.full_name sign bname;
- val full = Sign.full_name_path sign bname;
+ val name = Sign.full_name thy bname;
+ val full = Sign.full_name_path thy bname;
val base = Sign.base_name;
val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields);
@@ -2172,15 +2169,14 @@
fun gen_add_record prep_typ prep_raw_parent (params, bname) raw_parent raw_fields thy =
let
val _ = Theory.requires thy "Record" "record definitions";
- val sign = Theory.sign_of thy;
val _ = message ("Defining record " ^ quote bname ^ " ...");
(* parents *)
- fun prep_inst T = snd (cert_typ sign ([], T));
+ fun prep_inst T = snd (cert_typ thy ([], T));
- val parent = Option.map (apfst (map prep_inst) o prep_raw_parent sign) raw_parent
+ val parent = Option.map (apfst (map prep_inst) o prep_raw_parent thy) raw_parent
handle ERROR msg => cat_error msg ("The error(s) above in parent record specification");
val parents = add_parents thy parent [];
@@ -2193,7 +2189,7 @@
(* fields *)
fun prep_field (env, (c, raw_T, mx)) =
- let val (env', T) = prep_typ sign (env, raw_T) handle ERROR msg =>
+ let val (env', T) = prep_typ thy (env, raw_T) handle ERROR msg =>
cat_error msg ("The error(s) above occured in field " ^ quote c)
in (env', (c, T, mx)) end;
@@ -2203,13 +2199,13 @@
(* args *)
- val defaultS = Sign.defaultS sign;
+ val defaultS = Sign.defaultS thy;
val args = map (fn x => (x, AList.lookup (op =) envir x |> the_default defaultS)) params;
(* errors *)
- val name = Sign.full_name sign bname;
+ val name = Sign.full_name thy bname;
val err_dup_record =
if is_none (get_record thy name) then []
else ["Duplicate definition of record " ^ quote name];
--- a/src/HOL/Tools/res_atp.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Tools/res_atp.ML Wed Apr 04 00:11:03 2007 +0200
@@ -900,7 +900,7 @@
last_watcher_pid := SOME (childin, childout, pid, files);
Output.debug (fn () => "problem files: " ^ space_implode ", " files);
Output.debug (fn () => "pid: " ^ string_of_pid pid);
- watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
+ watcher_call_provers (Thm.theory_of_thm th) (Thm.prems_of th) (childin, childout, pid)
end;
(*For ML scripts, and primarily, for debugging*)
--- a/src/HOL/Tools/specification_package.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Tools/specification_package.ML Wed Apr 04 00:11:03 2007 +0200
@@ -32,7 +32,7 @@
Const("Ex",_) $ P =>
let
val ctype = domain_type (type_of P)
- val cname_full = Sign.intern_const (sign_of thy) cname
+ val cname_full = Sign.intern_const thy cname
val cdefname = if thname = ""
then Thm.def_name (Sign.base_name cname)
else thname
@@ -58,7 +58,7 @@
Const("Ex",_) $ P =>
let
val ctype = domain_type (type_of P)
- val cname_full = Sign.intern_const (sign_of thy) cname
+ val cname_full = Sign.intern_const thy cname
val cdefname = if thname = ""
then Thm.def_name (Sign.base_name cname)
else thname
@@ -183,7 +183,8 @@
in
thm RS spec'
end
- fun remove_alls frees thm = Library.foldl (inst_all (sign_of_thm thm)) (thm,frees)
+ fun remove_alls frees thm =
+ Library.foldl (inst_all (Thm.theory_of_thm thm)) (thm,frees)
fun process_single ((name,atts),rew_imp,frees) args =
let
fun undo_imps thm =
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Wed Apr 04 00:11:03 2007 +0200
@@ -55,7 +55,7 @@
param_tupel thy ((TFree(a,_))::r) res =
if (a mem res) then (param_tupel thy r res) else (param_tupel thy r (a::res)) |
param_tupel thy (a::r) res =
-error ("one component of a statetype is a TVar: " ^ (string_of_typ (sign_of thy) a));
+error ("one component of a statetype is a TVar: " ^ (string_of_typ thy a));
*)
(* used by constr_list *)
@@ -80,7 +80,7 @@
(* delivers constructor term string from a prem of *.induct *)
fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(Syntax.variant_abs(a,T,r)))|
extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r |
-extract_constr thy (Var(_,_) $ r) = delete_bold_string(string_of_term (sign_of thy) r) |
+extract_constr thy (Var(_,_) $ r) = delete_bold_string(string_of_term thy r) |
extract_constr _ _ = raise malformed;
in
(extract_hd a,extract_constr thy a) :: (extract_constrs thy r)
@@ -91,7 +91,7 @@
let
fun act_name thy (Type(s,_)) = s |
act_name _ s =
-error("malformed action type: " ^ (string_of_typ (sign_of thy) s));
+error("malformed action type: " ^ (string_of_typ thy s));
fun afpl ("." :: a) = [] |
afpl [] = [] |
afpl (a::r) = a :: (afpl r);
@@ -132,7 +132,7 @@
(* making a constructor set from a constructor term (of signature) *)
fun constr_set_string thy atyp ctstr =
let
-val trm = #t(rep_cterm(read_cterm (sign_of thy) (ctstr,atyp)));
+val trm = #t(rep_cterm(read_cterm thy (ctstr,atyp)));
val l = free_vars_of trm
in
if (check_for_constr thy atyp trm) then
@@ -140,7 +140,7 @@
else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})")
else (raise malformed)
handle malformed =>
-error("malformed action term: " ^ (string_of_term (sign_of thy) trm))
+error("malformed action term: " ^ (string_of_term thy trm))
end;
(* extracting constructor heads *)
@@ -149,7 +149,7 @@
fun hd_of (Const(a,_)) = a |
hd_of (t $ _) = hd_of t |
hd_of _ = raise malformed;
-val trm = #t(rep_cterm(read_cterm (sign_of thy) (s,#T(rep_ctyp(read_ctyp (sign_of thy) atypstr))) ))
+val trm = #t(rep_cterm(read_cterm thy (s,#T(rep_ctyp(read_ctyp thy atypstr))) ))
in
hd_of trm handle malformed =>
error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s)
@@ -177,8 +177,8 @@
(where bool indicates whether there is a precondition *)
fun extend thy atyp statetupel (actstr,r,[]) =
let
-val trm = #t(rep_cterm(read_cterm (sign_of thy) (actstr,atyp)));
-val rtrm = #t(rep_cterm(read_cterm (sign_of thy) (r,Type("bool",[]))));
+val trm = #t(rep_cterm(read_cterm thy (actstr,atyp)));
+val rtrm = #t(rep_cterm(read_cterm thy (r,Type("bool",[]))));
val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
in
if (check_for_constr thy atyp trm)
@@ -191,8 +191,8 @@
fun pseudo_poststring [] = "" |
pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" |
pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r);
-val trm = #t(rep_cterm(read_cterm (sign_of thy) (actstr,atyp)));
-val rtrm = #t(rep_cterm(read_cterm (sign_of thy) (r,Type("bool",[]))));
+val trm = #t(rep_cterm(read_cterm thy (actstr,atyp)));
+val rtrm = #t(rep_cterm(read_cterm thy (r,Type("bool",[]))));
val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
in
if (check_for_constr thy atyp trm) then
@@ -237,7 +237,7 @@
error("Action " ^ b ^ " is not in automaton signature")
))) else (write_alt thy (chead,ctrm) inp out int r)
handle malformed =>
-error ("malformed action term: " ^ (string_of_term (sign_of thy) a))
+error ("malformed action term: " ^ (string_of_term thy a))
end;
(* used by make_alt_string *)
@@ -286,16 +286,16 @@
left_of _ = raise malformed;
val aut_def = concl_of (get_thm thy (Name (aut_name ^ "_def")));
in
-(#T(rep_cterm(cterm_of (sign_of thy) (left_of aut_def))))
+(#T(rep_cterm(cterm_of thy (left_of aut_def))))
handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def")
end;
fun act_type_of thy (Type(pair1,(Type(pair_asig,(Type(actionset,[acttyp])::_))::_))) = acttyp |
act_type_of thy t = error ("could not extract action type of following automaton type:\n" ^
-(string_of_typ (sign_of thy) t));
+(string_of_typ thy t));
fun st_type_of thy (Type(pair1,_::(Type(pair2,Type(initial_set,[statetyp])::_))::_)) = statetyp |
st_type_of thy t = error ("could not extract state type of following automaton type:\n" ^
-(string_of_typ (sign_of thy) t));
+(string_of_typ thy t));
fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) |
comp_st_type_of thy (a::r) = Type("*",[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) |
@@ -330,10 +330,10 @@
(writeln("Constructing automaton " ^ automaton_name ^ " ...");
let
val state_type_string = type_product_of_varlist(statetupel);
-val styp = #T(rep_ctyp (read_ctyp (sign_of thy) state_type_string)) ;
+val styp = #T(rep_ctyp (read_ctyp thy state_type_string)) ;
val state_vars_tupel = "(" ^ (comma_list_of_varlist statetupel) ^ ")";
val state_vars_primed = "(" ^ (primed_comma_list_of_varlist statetupel) ^ ")";
-val atyp = #T(rep_ctyp (read_ctyp (sign_of thy) action_type));
+val atyp = #T(rep_ctyp (read_ctyp thy action_type));
val inp_set_string = action_set_string thy atyp inp;
val out_set_string = action_set_string thy atyp out;
val int_set_string = action_set_string thy atyp int;
@@ -364,7 +364,7 @@
automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^
"_initial, " ^ automaton_name ^ "_trans,{},{})")
])
-val chk_prime_list = (check_free_primed (#t(rep_cterm(read_cterm (sign_of thy2)
+val chk_prime_list = (check_free_primed (#t(rep_cterm(read_cterm thy2
( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string),Type("bool",[]))))));
in
(
--- a/src/HOLCF/adm_tac.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOLCF/adm_tac.ML Wed Apr 04 00:11:03 2007 +0200
@@ -150,7 +150,7 @@
NONE => no_tac
| SOME (s, T, t) =>
let
- val sign = sign_of_thm state;
+ val sign = Thm.theory_of_thm state;
val prems = Logic.strip_assums_hyp goali;
val params = Logic.strip_params goali;
val ts = find_subterms t 0 [];
--- a/src/HOLCF/domain/axioms.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOLCF/domain/axioms.ML Wed Apr 04 00:11:03 2007 +0200
@@ -14,7 +14,7 @@
infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<;
infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo;
-fun infer_types thy' = map (inferT_axm (sign_of thy'));
+fun infer_types thy' = map (inferT_axm thy');
fun calc_axioms comp_dname (eqs : eq list) n (((dname,_),cons) : eq)=
let
@@ -120,7 +120,7 @@
in (* local *)
fun add_axioms (comp_dnam, eqs : eq list) thy' = let
- val comp_dname = Sign.full_name (sign_of thy') comp_dnam;
+ val comp_dname = Sign.full_name thy' comp_dnam;
val dnames = map (fst o fst) eqs;
val x_name = idx_name dnames "x";
fun copy_app dname = %%:(dname^"_copy")`Bound 0;
--- a/src/HOLCF/domain/theorems.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOLCF/domain/theorems.ML Wed Apr 04 00:11:03 2007 +0200
@@ -99,14 +99,6 @@
val dist_eqI = prove_goal (the_context ()) "!!x::'a::po. ~ x << y ==> x ~= y"
(fn prems =>
[blast_tac (claset () addDs [antisym_less_inverse]) 1]);
-(*
-infixr 0 y;
-val b = 0;
-fun _ y t = by t;
-fun g defs t = let val sg = sign_of thy;
- val ct = Thm.cterm_of sg (inferT sg t);
- in goalw_cterm defs ct end;
-*)
in
@@ -201,7 +193,7 @@
val (n2, t2) = cons2typ n1 cons
in (n2, mk_ssumT (t1, t2)) end;
in
- fun cons2ctyp cons = ctyp_of (sign_of thy) (snd (cons2typ 1 cons));
+ fun cons2ctyp cons = ctyp_of thy (snd (cons2typ 1 cons));
end;
local
@@ -597,7 +589,7 @@
let
val dnames = map (fst o fst) eqs;
val conss = map snd eqs;
-val comp_dname = Sign.full_name (sign_of thy) comp_dnam;
+val comp_dname = Sign.full_name thy comp_dnam;
val d = writeln("Proving induction properties of domain "^comp_dname^" ...");
val pg = pg' thy;
@@ -877,7 +869,7 @@
else (* infinite case *)
let
fun one_finite n dn =
- read_instantiate_sg (sign_of thy)
+ read_instantiate_sg thy
[("P",dn^"_finite "^x_name n)] excluded_middle;
val finites = mapn one_finite 1 dnames;
--- a/src/Provers/Arith/fast_lin_arith.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Wed Apr 04 00:11:03 2007 +0200
@@ -773,7 +773,7 @@
val Hs = Logic.strip_assums_hyp A
val concl = Logic.strip_assums_concl A
in trace_thm ("Trying to refute subgoal " ^ string_of_int i) st;
- case prove (Thm.sign_of_thm st) params show_ex true Hs concl of
+ case prove (Thm.theory_of_thm st) params show_ex true Hs concl of
NONE => (trace_msg "Refutation failed."; no_tac)
| SOME js => (trace_msg "Refutation succeeded."; refute_tac ss (i, js))
end) i st;
--- a/src/Provers/IsaPlanner/isand.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/Provers/IsaPlanner/isand.ML Wed Apr 04 00:11:03 2007 +0200
@@ -23,12 +23,6 @@
ordering of proof, thus allowing proof attempts in parrell, but
recording the order to apply things in.
- debugging tools:
-
- fun asm_mk t = (assume (cterm_of (Theory.sign_of (the_context())) t));
- fun asm_read s =
- (assume (read_cterm (Theory.sign_of (Context.the_context())) (s,propT)));
-
THINK: are we really ok with our varify name w.r.t the prop - do
we also need to avoid names in the hidden hyps? What about
unification contraints in flex-flex pairs - might they also have
@@ -156,7 +150,7 @@
end;
fun allify_conditions' Ts th =
- allify_conditions (Thm.cterm_of (Thm.sign_of_thm th)) Ts th;
+ allify_conditions (Thm.cterm_of (Thm.theory_of_thm th)) Ts th;
(* allify types *)
fun allify_typ ts ty =
@@ -210,7 +204,7 @@
in renamings end;
fun fix_tvars_to_tfrees th =
let
- val sign = Thm.sign_of_thm th;
+ val sign = Thm.theory_of_thm th;
val ctypify = Thm.ctyp_of sign;
val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
val renamings = fix_tvars_to_tfrees_in_terms
@@ -243,7 +237,7 @@
in renamings end;
fun fix_vars_to_frees th =
let
- val ctermify = Thm.cterm_of (Thm.sign_of_thm th)
+ val ctermify = Thm.cterm_of (Thm.theory_of_thm th)
val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
val renamings = fix_vars_to_frees_in_terms
[] ([Thm.prop_of th] @ tpairs);
@@ -255,7 +249,7 @@
fun fix_tvars_upto_idx ix th =
let
- val sgn = Thm.sign_of_thm th;
+ val sgn = Thm.theory_of_thm th;
val ctypify = Thm.ctyp_of sgn
val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
val prop = (Thm.prop_of th);
@@ -268,7 +262,7 @@
in Thm.instantiate (ctyfixes, []) th end;
fun fix_vars_upto_idx ix th =
let
- val sgn = Thm.sign_of_thm th;
+ val sgn = Thm.theory_of_thm th;
val ctermify = Thm.cterm_of sgn
val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
val prop = (Thm.prop_of th);
@@ -334,7 +328,7 @@
fun export_back (export {fixes = vs, assumes = hprems,
sgid = i, gth = gth}) newth =
let
- val sgn = Thm.sign_of_thm newth;
+ val sgn = Thm.theory_of_thm newth;
val ctermify = Thm.cterm_of sgn;
val sgs = prems_of newth;
@@ -370,7 +364,7 @@
*)
fun prepare_goal_export (vs, cterms) th =
let
- val sgn = Thm.sign_of_thm th;
+ val sgn = Thm.theory_of_thm th;
val ctermify = Thm.cterm_of sgn;
val allfrees = map Term.dest_Free (Term.term_frees (Thm.prop_of th))
@@ -454,7 +448,7 @@
fun fix_alls_cterm i th =
let
- val ctermify = Thm.cterm_of (Thm.sign_of_thm th);
+ val ctermify = Thm.cterm_of (Thm.theory_of_thm th);
val (fixedbody, fvs) = fix_alls_term i (Thm.prop_of th);
val cfvs = rev (map ctermify fvs);
val ct_body = ctermify fixedbody
@@ -531,7 +525,7 @@
val prems = Logic.strip_imp_prems body;
val concl = Logic.strip_imp_concl body;
- val sgn = Thm.sign_of_thm th;
+ val sgn = Thm.theory_of_thm th;
val ctermify = Thm.cterm_of sgn;
val cprems = map ctermify prems;
val aprems = map Thm.assume cprems;
@@ -585,7 +579,7 @@
val prems = Logic.strip_imp_prems t;
- val sgn = Thm.sign_of_thm th;
+ val sgn = Thm.theory_of_thm th;
val ctermify = Thm.cterm_of sgn;
val aprems = map (Thm.trivial o ctermify) prems;
--- a/src/Provers/IsaPlanner/rw_inst.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/Provers/IsaPlanner/rw_inst.ML Wed Apr 04 00:11:03 2007 +0200
@@ -101,7 +101,7 @@
(* Note, we take abstraction in the order of last abstraction first *)
fun mk_abstractedrule TsFake Ts rule =
let
- val ctermify = Thm.cterm_of (Thm.sign_of_thm rule);
+ val ctermify = Thm.cterm_of (Thm.theory_of_thm rule);
(* now we change the names of temporary free vars that represent
bound vars with binders outside the redex *)
@@ -225,7 +225,7 @@
fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm =
let
(* general signature info *)
- val target_sign = (Thm.sign_of_thm target_thm);
+ val target_sign = (Thm.theory_of_thm target_thm);
val ctermify = Thm.cterm_of target_sign;
val ctypeify = Thm.ctyp_of target_sign;
--- a/src/Provers/eqsubst.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/Provers/eqsubst.ML Wed Apr 04 00:11:03 2007 +0200
@@ -338,7 +338,7 @@
val th = Thm.incr_indexes 1 gth;
val tgt_term = Thm.prop_of th;
- val sgn = Thm.sign_of_thm th;
+ val sgn = Thm.theory_of_thm th;
val ctermify = Thm.cterm_of sgn;
val trivify = Thm.trivial o ctermify;
@@ -448,7 +448,7 @@
val th = Thm.incr_indexes 1 gth;
val tgt_term = Thm.prop_of th;
- val sgn = Thm.sign_of_thm th;
+ val sgn = Thm.theory_of_thm th;
val ctermify = Thm.cterm_of sgn;
val trivify = Thm.trivial o ctermify;
--- a/src/Provers/order.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/Provers/order.ML Wed Apr 04 00:11:03 2007 +0200
@@ -77,7 +77,7 @@
(* Extract subgoal with signature *)
fun SUBGOAL goalfun i st =
- goalfun (List.nth(prems_of st, i-1), i, sign_of_thm st) st
+ goalfun (List.nth(prems_of st, i-1), i, Thm.theory_of_thm st) st
handle Subscript => Seq.empty;
(* Internal datatype for the proof *)
--- a/src/Provers/quasi.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/Provers/quasi.ML Wed Apr 04 00:11:03 2007 +0200
@@ -77,7 +77,7 @@
(* Extract subgoal with signature *)
fun SUBGOAL goalfun i st =
- goalfun (List.nth(prems_of st, i-1), i, sign_of_thm st) st
+ goalfun (List.nth(prems_of st, i-1), i, Thm.theory_of_thm st) st
handle Subscript => Seq.empty;
(* Internal datatype for the proof *)
--- a/src/Provers/splitter.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/Provers/splitter.ML Wed Apr 04 00:11:03 2007 +0200
@@ -322,7 +322,7 @@
fun inst_lift Ts t (T, U, pos) state i =
let
- val cert = cterm_of (sign_of_thm state);
+ val cert = cterm_of (Thm.theory_of_thm state);
val cntxt = mk_cntxt Ts t pos (T --> U) (#maxidx(rep_thm trlift));
in cterm_instantiate [(cert P, cert cntxt)] trlift
end;
@@ -346,7 +346,7 @@
val thm' = Thm.lift_rule (Thm.cprem_of state i) thm;
val (P, _) = strip_comb (fst (Logic.dest_equals
(Logic.strip_assums_concl (#prop (rep_thm thm')))));
- val cert = cterm_of (sign_of_thm state);
+ val cert = cterm_of (Thm.theory_of_thm state);
val cntxt = mk_cntxt_splitthm t tt TB;
val abss = Library.foldl (fn (t, T) => Abs ("", T, t));
in cterm_instantiate [(cert P, cert (abss (cntxt, Ts)))] thm'
--- a/src/Pure/theory.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/Pure/theory.ML Wed Apr 04 00:11:03 2007 +0200
@@ -7,7 +7,6 @@
signature BASIC_THEORY =
sig
- val sign_of: theory -> theory (*obsolete*)
val rep_theory: theory ->
{axioms: term NameSpace.table,
defs: Defs.T,
@@ -85,8 +84,6 @@
(* signature operations *)
-val sign_of = I;
-
structure SignTheory: SIGN_THEORY = Sign;
open SignTheory;
--- a/src/ZF/Tools/datatype_package.ML Wed Apr 04 00:10:59 2007 +0200
+++ b/src/ZF/Tools/datatype_package.ML Wed Apr 04 00:11:03 2007 +0200
@@ -55,18 +55,17 @@
val dummy = assert_all is_Const rec_hds
(fn t => "Datatype set not previously declared as constant: " ^
- Sign.string_of_term (sign_of thy) t);
+ Sign.string_of_term thy t);
val rec_names = map (#1 o dest_Const) rec_hds
val rec_base_names = map Sign.base_name rec_names
val big_rec_base_name = space_implode "_" rec_base_names
val thy_path = thy |> Theory.add_path big_rec_base_name
- val sign = sign_of thy_path
- val big_rec_name = Sign.intern_const sign big_rec_base_name;
+ val big_rec_name = Sign.intern_const thy_path big_rec_base_name;
- val intr_tms = Ind_Syntax.mk_all_intr_tms sign (rec_tms, con_ty_lists);
+ val intr_tms = Ind_Syntax.mk_all_intr_tms thy_path (rec_tms, con_ty_lists);
val dummy =
writeln ((if coind then "Codatatype" else "Datatype") ^ " definition " ^ quote big_rec_name);
@@ -84,7 +83,7 @@
val npart = length rec_names; (*number of mutually recursive parts*)
- val full_name = Sign.full_name sign;
+ val full_name = Sign.full_name thy_path;
(*Make constructor definition;
kpart is the number of this mutually recursive part*)
@@ -263,7 +262,7 @@
FOLogic.mk_Trueprop
(FOLogic.mk_eq
(case_tm $
- (list_comb (Const (Sign.intern_const (sign_of thy1) name,T),
+ (list_comb (Const (Sign.intern_const thy1 name,T),
args)),
list_comb (case_free, args)));
@@ -306,7 +305,7 @@
FOLogic.mk_Trueprop
(FOLogic.mk_eq
(recursor_tm $
- (list_comb (Const (Sign.intern_const (sign_of thy1) name,T),
+ (list_comb (Const (Sign.intern_const thy1 name,T),
args)),
subst_rec (Term.betapplys (recursor_case, args))));