# HG changeset patch
# User wenzelm
# Date 1154550409 -7200
# Node ID 8b3e97502fd9031ffbb6331be2d1507e8cd10030
# Parent  a69cda724b5af39eb8f61796718a0bb05bbd8355
use proper RecdefPackage.get_hints;
tuned;

diff -r a69cda724b5a -r 8b3e97502fd9 src/HOL/Tools/function_package/auto_term.ML
--- 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
-
-
-
-