# HG changeset patch
# User krauss
# Date 1161868591 -7200
# Node ID b6ab939147eb03cb31a4f581b23488af5bbad918
# Parent  367b4ad7c7cc83fd5d071e9df6bb5d5b4a753dfe
removed free "x" from termination goal...

diff -r 367b4ad7c7cc -r b6ab939147eb src/HOL/Tools/function_package/auto_term.ML
--- a/src/HOL/Tools/function_package/auto_term.ML	Thu Oct 26 15:12:03 2006 +0200
+++ b/src/HOL/Tools/function_package/auto_term.ML	Thu Oct 26 15:16:31 2006 +0200
@@ -28,7 +28,7 @@
     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 *)
+    rtac (Drule.cterm_instantiate [(R', rel')] rule') 1  (* instantiate termination rule *)
     THEN (ALLGOALS
       (fn 1 => REPEAT (ares_tac wf_rules 1)    (* Solve wellfoundedness *)
         | i => asm_simp_tac ss i))             (* Simplify termination conditions *)
@@ -42,9 +42,9 @@
 
     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)
+  in Method.SIMPLE_METHOD (auto_term_tac ctxt intro_rule rel wfs ss) end)
 
 val setup = Method.add_methods
-  [("auto_term", termination_meth, "termination prover for recdef compatibility")]
+  [("auto_term", termination_meth, "proves termination using a user-specified wellfounded relation")]
 
 end
diff -r 367b4ad7c7cc -r b6ab939147eb src/HOL/Tools/function_package/termination.ML
--- a/src/HOL/Tools/function_package/termination.ML	Thu Oct 26 15:12:03 2006 +0200
+++ b/src/HOL/Tools/function_package/termination.ML	Thu Oct 26 15:16:31 2006 +0200
@@ -26,7 +26,7 @@
 	val domT = domain_type (fastype_of f)
 	val x = Free ("x", domT)
     in
-      Trueprop (mk_acc domT R $ x)
+      mk_forall x (Trueprop (mk_acc domT R $ x))
     end
 
 fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _) dom =