--- a/src/HOL/HOL.thy Thu Nov 19 08:25:54 2009 +0100
+++ b/src/HOL/HOL.thy Thu Nov 19 08:25:57 2009 +0100
@@ -2060,7 +2060,6 @@
setup {*
Predicate_Compile_Alternative_Defs.setup
#> Predicate_Compile_Inline_Defs.setup
- #> Predicate_Compile_Preproc_Const_Defs.setup
*}
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Nov 19 08:25:54 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Nov 19 08:25:57 2009 +0100
@@ -137,7 +137,7 @@
th'
end
-fun store_thm_in_table options ignore_consts thy th=
+fun store_thm_in_table options ignore thy th=
let
val th = th
|> inline_equations options thy
@@ -153,29 +153,29 @@
else if (is_introlike th) then (defining_const_of_introrule th, th)
else error "store_thm: unexpected definition format"
in
- if not (member (op =) ignore_consts const) then
- Symtab.cons_list (const, th)
- else I
+ if ignore const then I else Symtab.cons_list (const, th)
end
fun make_const_spec_table options thy =
let
- fun store ignore_const f =
- fold (store_thm_in_table options ignore_const thy)
+ fun store ignore f =
+ fold (store_thm_in_table options ignore thy)
(map (Thm.transfer thy) (f (ProofContext.init thy)))
val table = Symtab.empty
- |> store [] Predicate_Compile_Alternative_Defs.get
- val ignore_consts = Symtab.keys table
+ |> store (K false) Predicate_Compile_Alternative_Defs.get
+ val ignore = Symtab.defined table
in
table
- |> store ignore_consts Predicate_Compile_Preproc_Const_Defs.get
- |> store ignore_consts Nitpick_Simps.get
- |> store ignore_consts Nitpick_Intros.get
+ |> store ignore (fn ctxt => maps
+ (fn (roughly, (ts, ths)) => if roughly = Spec_Rules.Equational then ths else [])
+ (Spec_Rules.get ctxt))
+ |> store ignore Nitpick_Simps.get
+ |> store ignore Nitpick_Intros.get
end
fun get_specification table constname =
case Symtab.lookup table constname of
- SOME thms => thms
+ SOME thms => thms
| NONE => error ("get_specification: lookup of constant " ^ quote constname ^ " failed")
val logic_operator_names =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Nov 19 08:25:54 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Nov 19 08:25:57 2009 +0100
@@ -83,7 +83,7 @@
val intro = Goal.prove (ProofContext.init thy') (map fst vs') [] t tac
val _ = tracing (Display.string_of_thm ctxt' intro)
val thy'' = thy'
- |> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro)
+ |> Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro)
|> Predicate_Compile.preprocess options full_constname
|> Predicate_Compile_Core.add_equations options [full_constname]
(* |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*)
--- a/src/Pure/Isar/code.ML Thu Nov 19 08:25:54 2009 +0100
+++ b/src/Pure/Isar/code.ML Thu Nov 19 08:25:57 2009 +0100
@@ -775,49 +775,4 @@
end;
-(** datastructure to log definitions for preprocessing of the predicate compiler **)
-(* obviously a clone of Named_Thms *)
-
-signature PREDICATE_COMPILE_PREPROC_CONST_DEFS =
-sig
- val get: Proof.context -> thm list
- val add_thm: thm -> Context.generic -> Context.generic
- val del_thm: thm -> Context.generic -> Context.generic
-
- val add_attribute : attribute
- val del_attribute : attribute
-
- val add_attrib : Attrib.src
-
- val setup: theory -> theory
-end;
-
-structure Predicate_Compile_Preproc_Const_Defs : PREDICATE_COMPILE_PREPROC_CONST_DEFS =
-struct
-
-structure Data = Generic_Data
-(
- type T = thm list;
- val empty = [];
- val extend = I;
- val merge = Thm.merge_thms;
-);
-
-val get = Data.get o Context.Proof;
-
-val add_thm = Data.map o Thm.add_thm;
-val del_thm = Data.map o Thm.del_thm;
-
-val add_attribute = Thm.declaration_attribute add_thm;
-val del_attribute = Thm.declaration_attribute del_thm;
-
-val add_attrib = Attrib.internal (K add_attribute)
-
-val setup =
- Attrib.setup (Binding.name "pred_compile_preproc") (Attrib.add_del add_attribute del_attribute)
- ("declaration of definition for preprocessing of the predicate compiler") #>
- PureThy.add_thms_dynamic (Binding.name "pred_compile_preproc", Data.get);
-
-end;
-
structure Code : CODE = struct open Code; end;
--- a/src/Pure/Isar/constdefs.ML Thu Nov 19 08:25:54 2009 +0100
+++ b/src/Pure/Isar/constdefs.ML Thu Nov 19 08:25:57 2009 +0100
@@ -55,8 +55,7 @@
|> PureThy.add_defs false [((name, def), atts)]
|-> (fn [thm] => (* FIXME thm vs. atts !? *)
Spec_Rules.add_global Spec_Rules.Equational ([Logic.varify head], [thm]) #>
- Code.add_default_eqn thm #>
- Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm thm));
+ Code.add_default_eqn thm);
in ((c, T), thy') end;
fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy =
--- a/src/Pure/Isar/specification.ML Thu Nov 19 08:25:54 2009 +0100
+++ b/src/Pure/Isar/specification.ML Thu Nov 19 08:25:57 2009 +0100
@@ -212,8 +212,7 @@
val ([(def_name, [th'])], lthy4) = lthy3
|> Local_Theory.notes_kind Thm.definitionK
- [((name, Predicate_Compile_Preproc_Const_Defs.add_attrib ::
- Code.add_default_eqn_attrib :: atts), [([th], [])])];
+ [((name, Code.add_default_eqn_attrib :: atts), [([th], [])])];
val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;
val _ =