--- 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 #>