# HG changeset patch
# User wenzelm
# Date 1160177461 -7200
# Node ID 4066ee15b278ef106cf425c55db41226c5e262e8
# Parent  528054ca23e321e288838450788dd58b966c6957
tuned method syntax: polymorhic term argument;
tuned rule instantiation;

diff -r 528054ca23e3 -r 4066ee15b278 src/HOL/Tools/function_package/auto_term.ML
--- a/src/HOL/Tools/function_package/auto_term.ML	Sat Oct 07 01:30:58 2006 +0200
+++ b/src/HOL/Tools/function_package/auto_term.ML	Sat Oct 07 01:31:01 2006 +0200
@@ -2,50 +2,49 @@
     ID:         $Id$
     Author:     Alexander Krauss, TU Muenchen
 
-A package for general recursive function definitions. 
+A package for general recursive function definitions.
 The auto_term method.
 *)
 
 
 signature FUNDEF_AUTO_TERM =
 sig
-    val setup : theory -> theory
+  val setup: theory -> theory
 end
 
-structure FundefAutoTerm : FUNDEF_AUTO_TERM = 
+structure FundefAutoTerm : FUNDEF_AUTO_TERM =
 struct
 
 open FundefCommon
 open FundefAbbrev
 
 
-
-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 *)
+fun auto_term_tac ctxt rule rel wf_rules ss =
+  let
+    val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
 
-fun mk_termination_meth relstr ctxt =
-    let
-        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))
-    end
+    val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
+    val rule' = rule |> Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1)
+    val prem = #1 (Logic.dest_implies (Thm.prop_of rule'))
+    val R' = cert (Var (the_single (Term.add_vars prem [])))
+  in
+    resolve_tac [Drule.cterm_instantiate [(R', rel')] rule'] 1  (* produce the usual goals *)
+    THEN (ALLGOALS
+      (fn 1 => REPEAT (ares_tac wf_rules 1)    (* Solve wellfoundedness *)
+        | i => asm_simp_tac ss i))             (* Simplify termination conditions *)
+  end
 
 
+fun termination_meth src = Method.syntax Args.term src #> (fn (ctxt, rel) =>
+  let
+    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 ctxt intro_rule rel wfs ss)) end)
 
 val setup = Method.add_methods
-  [("auto_term", Method.simple_args Args.name mk_termination_meth,
-    "termination prover for recdef compatibility")]
+  [("auto_term", termination_meth, "termination prover for recdef compatibility")]
 
 end