--- a/src/HOL/Tools/function_package/auto_term.ML Wed Aug 02 22:26:48 2006 +0200
+++ b/src/HOL/Tools/function_package/auto_term.ML Wed Aug 02 22:26:49 2006 +0200
@@ -23,30 +23,29 @@
fun auto_term_tac tc_intro_rule relstr wf_rules ss =
(resolve_tac [tc_intro_rule] 1) (* produce the usual goals *)
THEN (instantiate_tac [("R", relstr)]) (* instantiate with the given relation *)
- THEN (ALLGOALS
- (fn 1 => REPEAT (ares_tac wf_rules 1) (* Solve wellfoundedness *)
- | i => asm_simp_tac ss i)) (* Simplify termination conditions *)
+ THEN (ALLGOALS
+ (fn 1 => REPEAT (ares_tac wf_rules 1) (* Solve wellfoundedness *)
+ | i => asm_simp_tac ss i)) (* Simplify termination conditions *)
fun mk_termination_meth relstr ctxt =
let
- val {simps, congs, wfs} = RecdefPackage.get_local_hints ctxt
- val ss = local_simpset_of ctxt addsimps simps
-
- val intro_rule = ProofContext.get_thm ctxt (Name "termination")
+ val {simps, congs, wfs} = RecdefPackage.get_hints (Context.Proof ctxt)
+ val ss = local_simpset_of ctxt addsimps simps
+
+ val intro_rule = ProofContext.get_thm ctxt (Name "termination")
+ (* FIXME avoid internal name lookup -- dynamic scoping! *)
in
- Method.RAW_METHOD (K (auto_term_tac
- intro_rule
- relstr
- wfs
- ss))
+ Method.RAW_METHOD (K (auto_term_tac
+ intro_rule
+ relstr
+ wfs
+ ss))
end
-val setup = Method.add_methods [("auto_term", Method.simple_args Args.name mk_termination_meth, "termination prover for recdef compatibility")]
+val setup = Method.add_methods
+ [("auto_term", Method.simple_args Args.name mk_termination_meth,
+ "termination prover for recdef compatibility")]
end
-
-
-
-