--- a/src/HOL/Algebra/ringsimp.ML Mon Jun 20 22:13:58 2005 +0200
+++ b/src/HOL/Algebra/ringsimp.ML Mon Jun 20 22:13:59 2005 +0200
@@ -82,9 +82,9 @@
("Non-commutative rings in proof context: " ^ commas non_comm_rings ^
"\nCommutative rings in proof context: " ^ commas comm_rings);
val simps =
- List.concat (map (fn s => ProofContext.get_thms ctxt (s ^ ".ring_simprules", NONE))
+ List.concat (map (fn s => ProofContext.get_thms ctxt (Name (s ^ ".ring_simprules")))
non_comm_rings) @
- List.concat (map (fn s => ProofContext.get_thms ctxt (s ^ ".cring_simprules", NONE))
+ List.concat (map (fn s => ProofContext.get_thms ctxt (Name (s ^ ".cring_simprules")))
comm_rings);
in Method.SIMPLE_METHOD' HEADGOAL (asm_full_simp_tac (cring_ss addsimps simps))
end;
--- a/src/HOL/Import/proof_kernel.ML Mon Jun 20 22:13:58 2005 +0200
+++ b/src/HOL/Import/proof_kernel.ML Mon Jun 20 22:13:59 2005 +0200
@@ -401,7 +401,7 @@
fun dom_rng (Type("fun",[dom,rng])) = (dom,rng)
| dom_rng _ = raise ERR "dom_rng" "Not a functional type"
-fun mk_thy_const thy Thy Name Ty = Const(intern_const_name Thy Name thy,Ty)
+fun mk_thy_const thy Thy Nam Ty = Const(intern_const_name Thy Nam thy,Ty)
local
fun get_type sg thyname name =
@@ -409,12 +409,12 @@
SOME ty => ty
| NONE => raise ERR "get_type" (name ^ ": No such constant")
in
-fun prim_mk_const thy Thy Name =
+fun prim_mk_const thy Thy Nam =
let
- val name = intern_const_name Thy Name thy
+ val name = intern_const_name Thy Nam thy
val cmaps = HOL4ConstMaps.get thy
in
- case StringPair.lookup(cmaps,(Thy,Name)) of
+ case StringPair.lookup(cmaps,(Thy,Nam)) of
SOME(_,_,SOME ty) => Const(name,ty)
| _ => Const(name,get_type (sign_of thy) Thy name)
end
@@ -1236,10 +1236,10 @@
SOME (SOME thmname) =>
let
val _ = message ("Looking for " ^ thmname)
- val th1 = (SOME (transform_error (PureThy.get_thm thy) (thmname, NONE))
+ val th1 = (SOME (transform_error (PureThy.get_thm thy) (Name thmname))
handle ERROR_MESSAGE _ =>
(case split_name thmname of
- SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy (listname, NONE),idx-1))
+ SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy (Name listname),idx-1))
handle _ => NONE)
| NONE => NONE))
in
--- a/src/HOL/Library/word_setup.ML Mon Jun 20 22:13:58 2005 +0200
+++ b/src/HOL/Library/word_setup.ML Mon Jun 20 22:13:59 2005 +0200
@@ -24,7 +24,7 @@
fun add_word thy =
let
(*lcp** val fast1_th = PureThy.get_thm thy "Word.fast_nat_to_bv_def"**)
- val fast2_th = PureThy.get_thm thy ("Word.fast_bv_to_nat_def", NONE)
+ val fast2_th = PureThy.get_thm thy (Name "Word.fast_bv_to_nat_def")
(*lcp** fun f sg thms (Const("Word.nat_to_bv",_) $ (Const("Numeral.number_of",_) $ t)) =
if num_is_usable t
then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("w",0),Type("Numeral.bin",[]))),cterm_of sg t)] fast1_th)
--- a/src/HOL/Modelcheck/mucke_oracle.ML Mon Jun 20 22:13:58 2005 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Mon Jun 20 22:13:59 2005 +0200
@@ -984,8 +984,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 sg (s ^ ".induct", NONE)));
- val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm sg (s ^ ".induct", NONE)));
+ val pl = param_types (concl_of (get_thm sg (Name (s ^ ".induct"))));
+ val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm sg (Name (s ^ ".induct"))));
val ntl = new_types l;
in
((a,l) :: (preprocess_td sg (ntl @ b) (a :: done)))
--- a/src/HOL/Tools/datatype_package.ML Mon Jun 20 22:13:58 2005 +0200
+++ b/src/HOL/Tools/datatype_package.ML Mon Jun 20 22:13:59 2005 +0200
@@ -339,7 +339,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 o rpair NONE)
+ map (get_thm Datatype_thy o Name)
["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"]
in (case (#distinct (datatype_info_err sg tname1)) of
QuickAndDirty => SOME (Thm.invoke_oracle
@@ -644,7 +644,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", NONE);
+ val size_thms = if no_size then [] else get_thms thy3 (Name "size");
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 Jun 20 22:13:58 2005 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Mon Jun 20 22:13:59 2005 +0200
@@ -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 o rpair NONE)
+ Lim_inject, Suml_inject, Sumr_inject] = map (get_thm Datatype_thy o Name)
["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", NONE),
- get_thm thy4 ("Rep_" ^ s ^ "_inverse", NONE),
- get_thm thy4 ("Rep_" ^ s, NONE))) new_type_names;
+ (get_thm thy4 (Name ("Abs_" ^ s ^ "_inverse")),
+ get_thm thy4 (Name ("Rep_" ^ s ^ "_inverse")),
+ get_thm thy4 (Name ("Rep_" ^ s)))) new_type_names;
(*------------------------------------------------*)
(* prove additional theorems: *)
--- a/src/HOL/Tools/inductive_package.ML Mon Jun 20 22:13:58 2005 +0200
+++ b/src/HOL/Tools/inductive_package.ML Mon Jun 20 22:13:59 2005 +0200
@@ -614,11 +614,11 @@
val sum_case_rewrites =
(if Context.theory_name thy = "Datatype" then
- PureThy.get_thms thy ("sum.cases", NONE)
+ PureThy.get_thms thy (Name "sum.cases")
else
(case ThyInfo.lookup_theory "Datatype" of
NONE => []
- | SOME thy' => PureThy.get_thms thy' ("sum.cases", NONE)))
+ | SOME thy' => PureThy.get_thms thy' (Name "sum.cases")))
|> map mk_meta_eq;
val (preds, ind_prems, mutual_ind_concl, factors) =
--- a/src/HOL/Tools/typedef_package.ML Mon Jun 20 22:13:58 2005 +0200
+++ b/src/HOL/Tools/typedef_package.ML Mon Jun 20 22:13:59 2005 +0200
@@ -97,7 +97,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 (map (rpair NONE) witn_names) @ witn_thms;
+ val thms = PureThy.get_thmss thy (map Name witn_names) @ witn_thms;
val tac =
witn1_tac THEN
TRY (rewrite_goals_tac (List.filter is_def thms)) THEN
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Mon Jun 20 22:13:58 2005 +0200
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Mon Jun 20 22:13:59 2005 +0200
@@ -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", NONE));
+val prem = prems_of (get_thm thy (Name (uq_atypstr ^ ".induct")));
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", NONE));
+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))))
handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def")
--- a/src/HOLCF/domain/interface.ML Mon Jun 20 22:13:58 2005 +0200
+++ b/src/HOLCF/domain/interface.ML Mon Jun 20 22:13:59 2005 +0200
@@ -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) ^ ", NONE)";
+ fun get dname name = "get_thm thy (PureThy.Name " ^ Library.quote (dname ^ "." ^ name) ^ ")";
fun gen_vals dname name = "val "^ name ^ " = get_thm" ^
(if hd (rev (Symbol.explode name)) = "s" then "s" else "")^
- " thy (" ^ Library.quote (dname ^ "." ^ name) ^ ", NONE);";
+ " thy (PureThy.Name " ^ Library.quote (dname ^ "." ^ name) ^ ");";
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 Jun 20 22:13:58 2005 +0200
+++ b/src/HOLCF/domain/theorems.ML Mon Jun 20 22:13:59 2005 +0200
@@ -63,7 +63,7 @@
(* ----- getting the axioms and definitions --------------------------------- *)
-local fun ga s dn = get_thm thy (dn ^ "." ^ s, NONE) in
+local fun ga s dn = get_thm thy (Name (dn ^ "." ^ s)) 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;
@@ -352,7 +352,7 @@
(* ----- getting the composite axiom and definitions ------------------------ *)
-local fun ga s dn = get_thm thy (dn ^ "." ^ s, NONE) in
+local fun ga s dn = get_thm thy (Name (dn ^ "." ^ s)) 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;
@@ -360,8 +360,8 @@
val ax_bisim_def = ga "bisim_def" comp_dnam;
end; (* local *)
-local fun gt s dn = get_thm thy (dn ^ "." ^ s, NONE);
- fun gts s dn = get_thms thy (dn ^ "." ^ s, NONE) in
+local fun gt s dn = get_thm thy (Name (dn ^ "." ^ s));
+ fun gts s dn = get_thms thy (Name (dn ^ "." ^ s)) in
val cases = map (gt "casedist" ) dnames;
val con_rews = List.concat (map (gts "con_rews" ) dnames);
val copy_rews = List.concat (map (gts "copy_rews") dnames);
--- a/src/Pure/Isar/find_theorems.ML Mon Jun 20 22:13:58 2005 +0200
+++ b/src/Pure/Isar/find_theorems.ML Mon Jun 20 22:13:59 2005 +0200
@@ -38,7 +38,7 @@
| read_criterion _ Intro = Intro
| read_criterion _ Elim = Elim
| read_criterion _ Dest = Dest
- | read_criterion ctxt (Simp str) =
+ | read_criterion ctxt (Simp str) =
Simp (hd (ProofContext.read_term_pats TypeInfer.logicT ctxt [str]))
| read_criterion ctxt (Pattern str) =
Pattern (hd (ProofContext.read_term_pats TypeInfer.logicT ctxt [str]));
@@ -70,15 +70,15 @@
val sg = ProofContext.sign_of ctxt;
val tsig = Sign.tsig_of sg;
- val is_nontrivial = is_Const o head_of o ObjectLogic.drop_judgment sg;
+ val is_nontrivial = is_Const o head_of o ObjectLogic.drop_judgment sg;
- fun matches pat =
- is_nontrivial pat andalso
+ fun matches pat =
+ is_nontrivial pat andalso
Pattern.matches tsig (if po then (pat,obj) else (obj,pat))
handle Pattern.MATCH => false;
val match_thm = matches o extract_term o Thm.prop_of
- in
+ in
List.exists match_thm (extract_thms thm)
end;
@@ -93,7 +93,7 @@
(*filter that just looks for a string in the name,
substring match only (no regexps are performed)*)
-fun filter_name str_pat ((name, _), _) = is_substring str_pat name;
+fun filter_name str_pat (thmref, _) = is_substring str_pat (PureThy.name_of_thmref thmref);
(* filter intro/elim/dest rules *)
@@ -121,8 +121,8 @@
hd o Logic.strip_imp_prems);
val prems = Logic.prems_of_goal goal 1;
in
- prems |>
- List.exists (fn prem =>
+ prems |>
+ List.exists (fn prem =>
is_matching_thm extract_elim ctxt true prem thm
andalso (check_thm ctxt) thm)
end;
--- a/src/Pure/Proof/extraction.ML Mon Jun 20 22:13:58 2005 +0200
+++ b/src/Pure/Proof/extraction.ML Mon Jun 20 22:13:59 2005 +0200
@@ -115,7 +115,7 @@
Pattern.unify (thy, env, [pairself (lookup rew) p])) (env', prems')
in SOME (Envir.norm_term env'' (inc (ren tm2)))
end handle Pattern.MATCH => NONE | Pattern.Unif => NONE)
- (sort (Int.compare o pairself fst)
+ (sort (int_ord o pairself fst)
(Net.match_term rules (Pattern.eta_contract tm)))
end;
@@ -774,7 +774,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, NONE), (vs, s1, s2))) xs) thy)));
+ (PureThy.get_thm thy (Name a), (vs, s1, s2))) xs) thy)));
val realizabilityP =
OuterSyntax.command "realizability"
@@ -789,7 +789,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 o rpair NONE)) xs) thy)));
+ (fn thy => extract (map (apfst (PureThy.get_thm thy o Name)) xs) thy)));
val _ = OuterSyntax.add_parsers [realizersP, realizabilityP, typeofP, extractP];
--- a/src/Pure/Thy/thy_parse.ML Mon Jun 20 22:13:58 2005 +0200
+++ b/src/Pure/Thy/thy_parse.ML Mon Jun 20 22:13:59 2005 +0200
@@ -523,7 +523,7 @@
(* standard sections *)
-fun mk_val ax = "val " ^ ax ^ " = PureThy.get_thm thy (" ^ Library.quote ax ^ ", NONE);";
+fun mk_val ax = "val " ^ ax ^ " = PureThy.get_thm thy (PureThy.Name " ^ Library.quote ax ^ ");";
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 Jun 20 22:13:58 2005 +0200
+++ b/src/Pure/axclass.ML Mon Jun 20 22:13:59 2005 +0200
@@ -417,7 +417,7 @@
Pretty.string_of_arity (Sign.pp thy) (t, Ss, [c]));
fun witnesses thy names thms =
- PureThy.get_thmss thy (map (rpair NONE) names) @
+ PureThy.get_thmss thy (map Name names) @
thms @
List.filter is_def (map snd (axioms_of thy));
--- a/src/Pure/goals.ML Mon Jun 20 22:13:58 2005 +0200
+++ b/src/Pure/goals.ML Mon Jun 20 22:13:59 2005 +0200
@@ -315,7 +315,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));
+ | NONE => get thy (Name name));
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 Jun 20 22:13:58 2005 +0200
+++ b/src/Pure/proof_general.ML Mon Jun 20 22:13:59 2005 +0200
@@ -715,7 +715,7 @@
local
val topthy = Toplevel.theory_of o Toplevel.get_state
- fun pthm thy name = print_thm (get_thm thy (name, NONE))
+ fun pthm thy name = print_thm (get_thm thy (Name name))
fun idvalue tp nm = ("idvalue",[("objtype",tp),("name",nm)])
in