# HG changeset patch # User wenzelm # Date 1175638263 -7200 # Node ID b0eb5652f210e57f0ce05ea0aac3ca1582917b8a # Parent 1a08fce385656b278b3ca671aa2a857b49a9423d removed obsolete sign_of/sign_of_thm; diff -r 1a08fce38565 -r b0eb5652f210 TFL/casesplit.ML --- 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. *) diff -r 1a08fce38565 -r b0eb5652f210 TFL/post.ML --- 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; diff -r 1a08fce38565 -r b0eb5652f210 TFL/tfl.ML --- 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 diff -r 1a08fce38565 -r b0eb5652f210 src/FOLP/simp.ML --- 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 *); diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Bali/Basis.thy --- 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)); *} diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Import/hol4rews.ML --- 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 diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Import/import_package.ML --- 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))) diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Import/import_syntax.ML --- 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 = diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Import/shuffler.ML --- 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 diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Integ/int_arith1.ML --- 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 diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Integ/nat_simprocs.ML --- 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 ***) diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Integ/presburger.ML --- 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*) diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Library/word_setup.ML --- 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 diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML --- 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 diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Nominal/nominal_package.ML --- 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))); diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Nominal/nominal_permeq.ML --- 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 []; diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Real/ferrante_rackoff.ML --- 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*) diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Real/float.ML --- 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 diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Tools/Presburger/presburger.ML --- 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*) diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Tools/datatype_abs_proofs.ML --- 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' diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Tools/datatype_aux.ML --- 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); diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Tools/datatype_codegen.ML --- 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; diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Tools/datatype_package.ML --- 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; diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Tools/datatype_prop.ML --- 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); diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Tools/datatype_realizer.ML --- 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); diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Tools/datatype_rep_proofs.ML --- 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 diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Tools/record_package.ML --- 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]; diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Tools/res_atp.ML --- 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*) diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Tools/specification_package.ML --- 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 = diff -r 1a08fce38565 -r b0eb5652f210 src/HOLCF/IOA/meta_theory/ioa_package.ML --- 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 ( diff -r 1a08fce38565 -r b0eb5652f210 src/HOLCF/adm_tac.ML --- 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 []; diff -r 1a08fce38565 -r b0eb5652f210 src/HOLCF/domain/axioms.ML --- 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; diff -r 1a08fce38565 -r b0eb5652f210 src/HOLCF/domain/theorems.ML --- 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; diff -r 1a08fce38565 -r b0eb5652f210 src/Provers/Arith/fast_lin_arith.ML --- 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; diff -r 1a08fce38565 -r b0eb5652f210 src/Provers/IsaPlanner/isand.ML --- 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; diff -r 1a08fce38565 -r b0eb5652f210 src/Provers/IsaPlanner/rw_inst.ML --- 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; diff -r 1a08fce38565 -r b0eb5652f210 src/Provers/eqsubst.ML --- 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; diff -r 1a08fce38565 -r b0eb5652f210 src/Provers/order.ML --- 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 *) diff -r 1a08fce38565 -r b0eb5652f210 src/Provers/quasi.ML --- 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 *) diff -r 1a08fce38565 -r b0eb5652f210 src/Provers/splitter.ML --- 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' diff -r 1a08fce38565 -r b0eb5652f210 src/Pure/theory.ML --- 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; diff -r 1a08fce38565 -r b0eb5652f210 src/ZF/Tools/datatype_package.ML --- 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))));