Adapted to modified interface of PureThy.get_thm(s).
--- a/src/HOL/Modelcheck/mucke_oracle.ML Mon Jan 24 17:56:18 2005 +0100
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Mon Jan 24 17:59:48 2005 +0100
@@ -981,8 +981,8 @@
val s = post_last_dot(fst(qtn a));
fun param_types ((Const("Trueprop",_)) $ (_ $ (Var(_,Type(_,t))))) = t |
param_types _ = error "malformed induct-theorem in preprocess_td";
- val pl = param_types (concl_of (get_thm (theory_of_sign sg) (s ^ ".induct")));
- val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm (theory_of_sign sg) (s ^ ".induct")));
+ val pl = param_types (concl_of (get_thm (theory_of_sign sg) (s ^ ".induct", None)));
+ val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm (theory_of_sign sg) (s ^ ".induct", None)));
val ntl = new_types l;
in
((a,l) :: (preprocess_td sg (ntl @ b) (a :: done)))
--- a/src/HOL/Tools/datatype_package.ML Mon Jan 24 17:56:18 2005 +0100
+++ b/src/HOL/Tools/datatype_package.ML Mon Jan 24 17:59:48 2005 +0100
@@ -51,8 +51,8 @@
induction : thm,
size : thm list,
simps : thm list}
- val rep_datatype : string list option -> (xstring * Args.src list) list list ->
- (xstring * Args.src list) list list -> xstring * Args.src list -> theory -> theory *
+ val rep_datatype : string list option -> (thmref * Args.src list) list list ->
+ (thmref * Args.src list) list list -> thmref * Args.src list -> theory -> theory *
{distinct : thm list list,
inject : thm list list,
exhaustion : thm list,
@@ -355,7 +355,7 @@
val eq_ct = cterm_of sg eq_t;
val Datatype_thy = theory "Datatype";
val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] =
- map (get_thm Datatype_thy)
+ map (get_thm Datatype_thy o rpair None)
["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"]
in (case (#distinct (datatype_info_sg_err sg tname1)) of
QuickAndDirty => Some (Thm.invoke_oracle
@@ -583,21 +583,7 @@
(cname, map (typ_of_dtyp descr' sorts) cargs ---> T, mx))
(constrs ~~ constr_syntax')) ((hd descr) ~~ newTs ~~ constr_syntax);
- val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~
- replicate (length descr') HOLogic.typeS);
-
- val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
- map (fn (_, cargs) =>
- let
- val Ts = map (typ_of_dtyp descr' sorts) cargs;
- val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
-
- fun mk_argT (dt, T) =
- binder_types T ---> nth_elem (body_index dt, rec_result_Ts);
-
- val argTs = Ts @ map mk_argT recs
- in argTs ---> nth_elem (i, rec_result_Ts)
- end) constrs) descr');
+ val (rec_result_Ts, reccomb_fn_Ts) = DatatypeProp.make_primrec_Ts descr sorts used;
val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
val reccomb_names = if length descr' = 1 then [big_reccomb_name] else
@@ -674,7 +660,7 @@
Theory.parent_path |>>>
add_and_get_axiomss "inject" new_type_names
(DatatypeProp.make_injs descr sorts);
- val size_thms = if no_size then [] else get_thms thy3 "size";
+ val size_thms = if no_size then [] else get_thms thy3 ("size", None);
val (thy4, distinct) = add_and_get_axiomss "distinct" new_type_names
(DatatypeProp.make_distincts new_type_names descr sorts thy3) thy3;
--- a/src/HOL/Tools/datatype_rep_proofs.ML Mon Jan 24 17:56:18 2005 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Mon Jan 24 17:59:48 2005 +0100
@@ -57,7 +57,7 @@
val [In0_inject, In1_inject, Scons_inject, Leaf_inject,
In0_eq, In1_eq, In0_not_In1, In1_not_In0,
- Lim_inject, Suml_inject, Sumr_inject] = map (get_thm Datatype_thy)
+ Lim_inject, Suml_inject, Sumr_inject] = map (get_thm Datatype_thy o rpair None)
["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject",
"In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0",
"Lim_inject", "Suml_inject", "Sumr_inject"];
@@ -261,9 +261,9 @@
(* get axioms from theory *)
val newT_iso_axms = map (fn s =>
- (get_thm thy4 ("Abs_" ^ s ^ "_inverse"),
- get_thm thy4 ("Rep_" ^ s ^ "_inverse"),
- get_thm thy4 ("Rep_" ^ s))) new_type_names;
+ (get_thm thy4 ("Abs_" ^ s ^ "_inverse", None),
+ get_thm thy4 ("Rep_" ^ s ^ "_inverse", None),
+ get_thm thy4 ("Rep_" ^ s, None))) new_type_names;
(*------------------------------------------------*)
(* prove additional theorems: *)
--- a/src/HOL/Tools/typedef_package.ML Mon Jan 24 17:56:18 2005 +0100
+++ b/src/HOL/Tools/typedef_package.ML Mon Jan 24 17:59:48 2005 +0100
@@ -101,7 +101,7 @@
fun prove_nonempty thy cset goal (witn1_tac, witn_names, witn_thms, witn2_tac) =
let
val is_def = Logic.is_equals o #prop o Thm.rep_thm;
- val thms = PureThy.get_thmss thy witn_names @ witn_thms;
+ val thms = PureThy.get_thmss thy (map (rpair None) witn_names) @ witn_thms;
val tac =
witn1_tac THEN
TRY (rewrite_goals_tac (filter is_def thms)) THEN
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Mon Jan 24 17:56:18 2005 +0100
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Mon Jan 24 17:59:48 2005 +0100
@@ -98,7 +98,7 @@
fun unqualify s = implode(rev(afpl(rev(explode s))));
val q_atypstr = act_name thy atyp;
val uq_atypstr = unqualify q_atypstr;
-val prem = prems_of (get_thm thy (uq_atypstr ^ ".induct"));
+val prem = prems_of (get_thm thy (uq_atypstr ^ ".induct", None));
in
extract_constrs thy prem
handle malformed =>
@@ -284,7 +284,7 @@
let
fun left_of (( _ $ left) $ _) = left |
left_of _ = raise malformed;
-val aut_def = concl_of(get_thm thy (aut_name ^ "_def"));
+val aut_def = concl_of (get_thm thy (aut_name ^ "_def", None));
in
(#T(rep_cterm(cterm_of (sign_of thy) (left_of aut_def))))
handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def")
--- a/src/HOLCF/domain/interface.ML Mon Jan 24 17:56:18 2005 +0100
+++ b/src/HOLCF/domain/interface.ML Mon Jan 24 17:59:48 2005 +0100
@@ -12,10 +12,10 @@
(* --- generation of bindings for axioms and theorems in .thy.ML - *)
- fun get dname name = "get_thm thy " ^ Library.quote (dname^"."^name);
+ fun get dname name = "get_thm thy (" ^ Library.quote (dname ^ "." ^ name) ^ ", None)";
fun gen_vals dname name = "val "^ name ^ " = get_thm" ^
(if hd (rev (Symbol.explode name)) = "s" then "s" else "")^
- " thy " ^ Library.quote (dname^"."^name)^";";
+ " thy (" ^ Library.quote (dname ^ "." ^ name) ^ ", None);";
fun gen_vall name l = "val "^name^" = "^ mk_list l^";";
val rews = "iso_rews @ when_rews @\n\
\ con_rews @ sel_rews @ dis_rews @ dist_les @ dist_eqs @\n\
--- a/src/HOLCF/domain/theorems.ML Mon Jan 24 17:56:18 2005 +0100
+++ b/src/HOLCF/domain/theorems.ML Mon Jan 24 17:59:48 2005 +0100
@@ -65,7 +65,7 @@
(* ----- getting the axioms and definitions --------------------------------- *)
-local fun ga s dn = get_thm thy (dn^"."^s) in
+local fun ga s dn = get_thm thy (dn ^ "." ^ s, None) in
val ax_abs_iso = ga "abs_iso" dname;
val ax_rep_iso = ga "rep_iso" dname;
val ax_when_def = ga "when_def" dname;
@@ -341,7 +341,7 @@
(* ----- getting the composite axiom and definitions ------------------------ *)
-local fun ga s dn = get_thm thy (dn^"."^s) in
+local fun ga s dn = get_thm thy (dn ^ "." ^ s, None) in
val axs_reach = map (ga "reach" ) dnames;
val axs_take_def = map (ga "take_def" ) dnames;
val axs_finite_def = map (ga "finite_def") dnames;
@@ -349,8 +349,8 @@
val ax_bisim_def = ga "bisim_def" comp_dnam;
end; (* local *)
-local fun gt s dn = get_thm thy (dn^"."^s);
- fun gts s dn = get_thms thy (dn^"."^s) in
+local fun gt s dn = get_thm thy (dn ^ "." ^ s, None);
+ fun gts s dn = get_thms thy (dn ^ "." ^ s, None) in
val cases = map (gt "casedist" ) dnames;
val con_rews = flat (map (gts "con_rews" ) dnames);
val copy_rews = flat (map (gts "copy_rews") dnames);
--- a/src/Pure/Proof/extraction.ML Mon Jan 24 17:56:18 2005 +0100
+++ b/src/Pure/Proof/extraction.ML Mon Jan 24 17:59:48 2005 +0100
@@ -734,7 +734,7 @@
(Scan.repeat1 (P.xname -- parse_vars --| P.$$$ ":" -- P.string -- P.string) >>
(fn xs => Toplevel.theory (fn thy => add_realizers
(map (fn (((a, vs), s1), s2) =>
- (PureThy.get_thm thy a, (vs, s1, s2))) xs) thy)));
+ (PureThy.get_thm thy (a, None), (vs, s1, s2))) xs) thy)));
val realizabilityP =
OuterSyntax.command "realizability"
@@ -749,7 +749,7 @@
val extractP =
OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl
(Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory
- (fn thy => extract (map (apfst (PureThy.get_thm thy)) xs) thy)));
+ (fn thy => extract (map (apfst (PureThy.get_thm thy o rpair None)) xs) thy)));
val parsers = [realizersP, realizabilityP, typeofP, extractP];
--- a/src/Pure/Thy/thy_parse.ML Mon Jan 24 17:56:18 2005 +0100
+++ b/src/Pure/Thy/thy_parse.ML Mon Jan 24 17:59:48 2005 +0100
@@ -523,7 +523,7 @@
(* standard sections *)
-fun mk_val ax = "val " ^ ax ^ " = PureThy.get_thm thy " ^ Library.quote ax ^ ";";
+fun mk_val ax = "val " ^ ax ^ " = PureThy.get_thm thy (" ^ Library.quote ax ^ ", None);";
val mk_vals = cat_lines o map mk_val;
fun mk_axm_sect "" (txt, axs) = (txt, mk_vals axs)
--- a/src/Pure/axclass.ML Mon Jan 24 17:56:18 2005 +0100
+++ b/src/Pure/axclass.ML Mon Jan 24 17:59:48 2005 +0100
@@ -64,7 +64,7 @@
val is_def = Logic.is_equals o #prop o rep_thm;
fun witnesses thy names thms =
- PureThy.get_thmss thy names @ thms @ filter is_def (map snd (axioms_of thy));
+ PureThy.get_thmss thy (map (rpair None) names) @ thms @ filter is_def (map snd (axioms_of thy));
--- a/src/Pure/goals.ML Mon Jan 24 17:56:18 2005 +0100
+++ b/src/Pure/goals.ML Mon Jan 24 17:59:48 2005 +0100
@@ -330,7 +330,7 @@
fun get_thmx f get thy name =
(case get_first (get_thm_locale name) (get_scope thy) of
Some thm => f thm
- | None => get thy name);
+ | None => get thy (name, None));
val get_thm = get_thmx I PureThy.get_thm;
val get_thms = get_thmx (fn x => [x]) PureThy.get_thms;
--- a/src/Pure/proof_general.ML Mon Jan 24 17:56:18 2005 +0100
+++ b/src/Pure/proof_general.ML Mon Jan 24 17:59:48 2005 +0100
@@ -685,7 +685,7 @@
local
val topthy = Toplevel.theory_of o Toplevel.get_state
- val pthm = print_thm oo get_thm
+ fun pthm thy name = print_thm (get_thm thy (name, None))
fun idvalue tp nm = ("idvalue",[("objtype",tp),("name",nm)])
in