--- a/src/HOL/Tools/Function/partial_function.ML Sat Aug 16 19:01:31 2014 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Sat Aug 16 19:20:11 2014 +0200
@@ -6,7 +6,6 @@
signature PARTIAL_FUNCTION =
sig
- val setup: theory -> theory
val init: string -> term -> term -> thm -> thm -> thm option -> declaration
val mono_tac: Proof.context -> int -> tactic
@@ -54,13 +53,6 @@
val lookup_mode = Symtab.lookup o Modes.get o Context.Proof;
-structure Mono_Rules = Named_Thms
-(
- val name = @{binding partial_function_mono};
- val description = "monotonicity rules for partial function definitions";
-);
-
-
(*** Automated monotonicity proofs ***)
fun strip_cases ctac = ctac #> Seq.map snd;
@@ -109,7 +101,7 @@
fun mono_tac ctxt =
K (Local_Defs.unfold_tac ctxt [@{thm curry_def}])
THEN' (TRY o REPEAT_ALL_NEW
- (resolve_tac (Mono_Rules.get ctxt)
+ (resolve_tac (rev (Named_Theorems.get ctxt @{named_theorems partial_function_mono}))
ORELSE' split_cases_tac ctxt));
@@ -321,7 +313,4 @@
((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
>> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
-
-val setup = Mono_Rules.setup;
-
end