src/HOL/Library/refute.ML
 changeset 56256 1e01c159e7d9 parent 56252 b72e0a9d62b9 child 56815 848d507584db
```     1.1 --- a/src/HOL/Library/refute.ML	Sat Mar 22 19:33:39 2014 +0100
1.2 +++ b/src/HOL/Library/refute.ML	Sat Mar 22 20:42:16 2014 +0100
1.3 @@ -4,11 +4,6 @@
1.4  Finite model generation for HOL formulas, using a SAT solver.
1.5  *)
1.6
1.7 -(* ------------------------------------------------------------------------- *)
1.8 -(* Declares the 'REFUTE' signature as well as a structure 'Refute'.          *)
1.9 -(* Documentation is available in the Isabelle/Isar theory 'HOL/Refute.thy'.  *)
1.10 -(* ------------------------------------------------------------------------- *)
1.11 -
1.12  signature REFUTE =
1.13  sig
1.14
1.15 @@ -638,6 +633,16 @@
1.16  (* To avoid collecting the same axiom multiple times, we use an           *)
1.17  (* accumulator 'axs' which contains all axioms collected so far.          *)
1.18
1.19 +local
1.20 +
1.21 +fun get_axiom thy xname =
1.22 +  Name_Space.check (Context.Theory thy) (Theory.axiom_table thy) (xname, Position.none);
1.23 +
1.24 +val the_eq_trivial = get_axiom @{theory HOL} "the_eq_trivial";
1.25 +val someI = get_axiom @{theory Hilbert_Choice} "someI";
1.26 +
1.27 +in
1.28 +
1.29  fun collect_axioms ctxt t =
1.30    let
1.31      val thy = Proof_Context.theory_of ctxt
1.32 @@ -724,17 +729,15 @@
1.33        | Const (@{const_name undefined}, T) => collect_type_axioms T axs
1.34        | Const (@{const_name The}, T) =>
1.35            let
1.36 -            val ax = specialize_type thy (@{const_name The}, T)
1.37 -              (the (AList.lookup (op =) axioms "HOL.the_eq_trivial"))
1.38 +            val ax = specialize_type thy (@{const_name The}, T) (#2 the_eq_trivial)
1.39            in
1.40 -            collect_this_axiom ("HOL.the_eq_trivial", ax) axs
1.41 +            collect_this_axiom (#1 the_eq_trivial, ax) axs
1.42            end
1.43        | Const (@{const_name Hilbert_Choice.Eps}, T) =>
1.44            let
1.45 -            val ax = specialize_type thy (@{const_name Hilbert_Choice.Eps}, T)
1.46 -              (the (AList.lookup (op =) axioms "Hilbert_Choice.someI"))
1.47 +            val ax = specialize_type thy (@{const_name Hilbert_Choice.Eps}, T) (#2 someI)
1.48            in
1.49 -            collect_this_axiom ("Hilbert_Choice.someI", ax) axs
1.50 +            collect_this_axiom (#1 someI, ax) axs
1.51            end
1.52        | Const (@{const_name All}, T) => collect_type_axioms T axs
1.53        | Const (@{const_name Ex}, T) => collect_type_axioms T axs
1.54 @@ -806,6 +809,8 @@
1.55      result
1.56    end;
1.57
1.58 +end;
1.59 +
1.60  (* ------------------------------------------------------------------------- *)
1.61  (* ground_types: collects all ground types in a term (including argument     *)
1.62  (*               types of other types), suppressing duplicates.  Does not    *)
1.63 @@ -3032,7 +3037,7 @@
1.64  (*       applied before the 'stlc_interpreter' breaks the term apart into    *)
1.65  (*       subterms that are then passed to other interpreters!                *)
1.66  (* ------------------------------------------------------------------------- *)
1.67 -
1.68 +(* FIXME formal @{const_name} for some entries (!??) *)
1.69  val setup =