--- a/src/HOL/Import/import_rule.ML Sat Mar 22 19:33:39 2014 +0100
+++ b/src/HOL/Import/import_rule.ML Sat Mar 22 20:42:16 2014 +0100
@@ -409,7 +409,7 @@
end
| process (thy, state) (#"Y", [name, _, _]) = setth (mtydef name thy) (thy, state)
| process (thy, state) (#"t", [n]) =
- setty (ctyp_of thy (TFree ("'" ^ (transl_qm n), ["HOL.type"]))) (thy, state)
+ setty (ctyp_of thy (TFree ("'" ^ (transl_qm n), @{sort type}))) (thy, state)
| process (thy, state) (#"a", n :: l) =
fold_map getty l (thy, state) |>>
(fn tys => ctyp_of thy (Type (gettyname n thy, map typ_of tys))) |-> setty
--- a/src/HOL/Library/refute.ML Sat Mar 22 19:33:39 2014 +0100
+++ b/src/HOL/Library/refute.ML Sat Mar 22 20:42:16 2014 +0100
@@ -4,11 +4,6 @@
Finite model generation for HOL formulas, using a SAT solver.
*)
-(* ------------------------------------------------------------------------- *)
-(* Declares the 'REFUTE' signature as well as a structure 'Refute'. *)
-(* Documentation is available in the Isabelle/Isar theory 'HOL/Refute.thy'. *)
-(* ------------------------------------------------------------------------- *)
-
signature REFUTE =
sig
@@ -638,6 +633,16 @@
(* To avoid collecting the same axiom multiple times, we use an *)
(* accumulator 'axs' which contains all axioms collected so far. *)
+local
+
+fun get_axiom thy xname =
+ Name_Space.check (Context.Theory thy) (Theory.axiom_table thy) (xname, Position.none);
+
+val the_eq_trivial = get_axiom @{theory HOL} "the_eq_trivial";
+val someI = get_axiom @{theory Hilbert_Choice} "someI";
+
+in
+
fun collect_axioms ctxt t =
let
val thy = Proof_Context.theory_of ctxt
@@ -724,17 +729,15 @@
| Const (@{const_name undefined}, T) => collect_type_axioms T axs
| Const (@{const_name The}, T) =>
let
- val ax = specialize_type thy (@{const_name The}, T)
- (the (AList.lookup (op =) axioms "HOL.the_eq_trivial"))
+ val ax = specialize_type thy (@{const_name The}, T) (#2 the_eq_trivial)
in
- collect_this_axiom ("HOL.the_eq_trivial", ax) axs
+ collect_this_axiom (#1 the_eq_trivial, ax) axs
end
| Const (@{const_name Hilbert_Choice.Eps}, T) =>
let
- val ax = specialize_type thy (@{const_name Hilbert_Choice.Eps}, T)
- (the (AList.lookup (op =) axioms "Hilbert_Choice.someI"))
+ val ax = specialize_type thy (@{const_name Hilbert_Choice.Eps}, T) (#2 someI)
in
- collect_this_axiom ("Hilbert_Choice.someI", ax) axs
+ collect_this_axiom (#1 someI, ax) axs
end
| Const (@{const_name All}, T) => collect_type_axioms T axs
| Const (@{const_name Ex}, T) => collect_type_axioms T axs
@@ -806,6 +809,8 @@
result
end;
+end;
+
(* ------------------------------------------------------------------------- *)
(* ground_types: collects all ground types in a term (including argument *)
(* types of other types), suppressing duplicates. Does not *)
@@ -3032,7 +3037,7 @@
(* applied before the 'stlc_interpreter' breaks the term apart into *)
(* subterms that are then passed to other interpreters! *)
(* ------------------------------------------------------------------------- *)
-
+(* FIXME formal @{const_name} for some entries (!??) *)
val setup =
add_interpreter "stlc" stlc_interpreter #>
add_interpreter "Pure" Pure_interpreter #>
--- a/src/HOL/NSA/StarDef.thy Sat Mar 22 19:33:39 2014 +0100
+++ b/src/HOL/NSA/StarDef.thy Sat Mar 22 20:42:16 2014 +0100
@@ -172,7 +172,7 @@
"Standard = range star_of"
text {* Transfer tactic should remove occurrences of @{term star_of} *}
-setup {* Transfer_Principle.add_const "StarDef.star_of" *}
+setup {* Transfer_Principle.add_const @{const_name star_of} *}
declare star_of_def [transfer_intro]
@@ -199,7 +199,7 @@
UN_equiv_class2 [OF equiv_starrel equiv_starrel Ifun_congruent2])
text {* Transfer tactic should remove occurrences of @{term Ifun} *}
-setup {* Transfer_Principle.add_const "StarDef.Ifun" *}
+setup {* Transfer_Principle.add_const @{const_name Ifun} *}
lemma transfer_Ifun [transfer_intro]:
"\<lbrakk>f \<equiv> star_n F; x \<equiv> star_n X\<rbrakk> \<Longrightarrow> f \<star> x \<equiv> star_n (\<lambda>n. F n (X n))"
@@ -306,7 +306,7 @@
by (simp add: unstar_def star_of_inject)
text {* Transfer tactic should remove occurrences of @{term unstar} *}
-setup {* Transfer_Principle.add_const "StarDef.unstar" *}
+setup {* Transfer_Principle.add_const @{const_name unstar} *}
lemma transfer_unstar [transfer_intro]:
"p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>"
@@ -348,7 +348,7 @@
by (simp add: Iset_def starP2_star_n)
text {* Transfer tactic should remove occurrences of @{term Iset} *}
-setup {* Transfer_Principle.add_const "StarDef.Iset" *}
+setup {* Transfer_Principle.add_const @{const_name Iset} *}
lemma transfer_mem [transfer_intro]:
"\<lbrakk>x \<equiv> star_n X; a \<equiv> Iset (star_n A)\<rbrakk>
--- a/src/HOL/NSA/transfer.ML Sat Mar 22 19:33:39 2014 +0100
+++ b/src/HOL/NSA/transfer.ML Sat Mar 22 20:42:16 2014 +0100
@@ -35,7 +35,7 @@
consts = Library.merge (op =) (consts1, consts2)};
);
-fun unstar_typ (Type ("StarDef.star",[t])) = unstar_typ t
+fun unstar_typ (Type (@{type_name star}, [t])) = unstar_typ t
| unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts)
| unstar_typ T = T
--- a/src/HOL/TLA/Action.thy Sat Mar 22 19:33:39 2014 +0100
+++ b/src/HOL/TLA/Action.thy Sat Mar 22 20:42:16 2014 +0100
@@ -117,7 +117,7 @@
fun action_use ctxt th =
case (concl_of th) of
- Const _ $ (Const ("Intensional.Valid", _) $ _) =>
+ Const _ $ (Const (@{const_name Valid}, _) $ _) =>
(flatten (action_unlift ctxt th) handle THM _ => th)
| _ => th;
*}
--- a/src/HOL/TLA/Intensional.thy Sat Mar 22 19:33:39 2014 +0100
+++ b/src/HOL/TLA/Intensional.thy Sat Mar 22 20:42:16 2014 +0100
@@ -283,7 +283,7 @@
fun int_use ctxt th =
case (concl_of th) of
- Const _ $ (Const ("Intensional.Valid", _) $ _) =>
+ Const _ $ (Const (@{const_name Valid}, _) $ _) =>
(flatten (int_unlift ctxt th) handle THM _ => th)
| _ => th
*}
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Sat Mar 22 19:33:39 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Sat Mar 22 20:42:16 2014 +0100
@@ -256,11 +256,11 @@
in
case thf_ty of
Prod_type (thf_ty1, thf_ty2) =>
- Type ("Product_Type.prod",
+ Type (@{type_name prod},
[interpret_type config thy type_map thf_ty1,
interpret_type config thy type_map thf_ty2])
| Fn_type (thf_ty1, thf_ty2) =>
- Type ("fun",
+ Type (@{type_name fun},
[interpret_type config thy type_map thf_ty1,
interpret_type config thy type_map thf_ty2])
| Atom_type _ =>
@@ -398,8 +398,7 @@
(*As above, but for products*)
fun mtimes thy =
fold (fn x => fn y =>
- Sign.mk_const thy
- ("Product_Type.Pair", [dummyT, dummyT]) $ y $ x)
+ Sign.mk_const thy (@{const_name Pair}, [dummyT, dummyT]) $ y $ x)
fun mtimes' (args, thy) f =
let
@@ -456,11 +455,11 @@
end
(*Next batch of functions give info about Isabelle/HOL types*)
-fun is_fun (Type ("fun", _)) = true
+fun is_fun (Type (@{type_name fun}, _)) = true
| is_fun _ = false
-fun is_prod (Type ("Product_Type.prod", _)) = true
+fun is_prod (Type (@{type_name prod}, _)) = true
| is_prod _ = false
-fun dom_type (Type ("fun", [ty1, _])) = ty1
+fun dom_type (Type (@{type_name fun}, [ty1, _])) = ty1
fun is_prod_typed thy config symb =
let
fun symb_type const_name =
--- a/src/HOL/ex/SVC_Oracle.thy Sat Mar 22 19:33:39 2014 +0100
+++ b/src/HOL/ex/SVC_Oracle.thy Sat Mar 22 20:42:16 2014 +0100
@@ -11,12 +11,12 @@
imports Main
begin
-ML_file "svc_funcs.ML"
-
consts
iff_keep :: "[bool, bool] => bool"
iff_unfold :: "[bool, bool] => bool"
+ML_file "svc_funcs.ML"
+
hide_const iff_keep iff_unfold
oracle svc_oracle = Svc.oracle
--- a/src/HOL/ex/svc_funcs.ML Sat Mar 22 19:33:39 2014 +0100
+++ b/src/HOL/ex/svc_funcs.ML Sat Mar 22 20:42:16 2014 +0100
@@ -199,10 +199,10 @@
Buildin("NOT", [fm (not pos) p])
| fm pos (Const(@{const_name True}, _)) = TrueExpr
| fm pos (Const(@{const_name False}, _)) = FalseExpr
- | fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) =
+ | fm pos (Const(@{const_name iff_keep}, _) $ p $ q) =
(*polarity doesn't matter*)
Buildin("=", [fm pos p, fm pos q])
- | fm pos (Const("SVC_Oracle.iff_unfold", _) $ p $ q) =
+ | fm pos (Const(@{const_name iff_unfold}, _) $ p $ q) =
Buildin("AND", (*unfolding uses both polarities*)
[Buildin("=>", [fm (not pos) p, fm pos q]),
Buildin("=>", [fm (not pos) q, fm pos p])])