# HG changeset patch
# User krauss
# Date 1256308676 -7200
# Node ID acc2bd3934baaae8dcd7d2bc76d52417b6689c9f
# Parent  b8cdd3d7302252a910ddef95ed220669d30fa8a7
renamed auto_term.ML -> relation.ML

diff -r b8cdd3d73022 -r acc2bd3934ba src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Fri Oct 23 16:22:10 2009 +0200
+++ b/src/HOL/FunDef.thy	Fri Oct 23 16:37:56 2009 +0200
@@ -18,7 +18,7 @@
   ("Tools/Function/mutual.ML")
   ("Tools/Function/pattern_split.ML")
   ("Tools/Function/function.ML")
-  ("Tools/Function/auto_term.ML")
+  ("Tools/Function/relation.ML")
   ("Tools/Function/measure_functions.ML")
   ("Tools/Function/lexicographic_order.ML")
   ("Tools/Function/pat_completeness.ML")
@@ -112,7 +112,7 @@
 use "Tools/Function/sum_tree.ML"
 use "Tools/Function/mutual.ML"
 use "Tools/Function/pattern_split.ML"
-use "Tools/Function/auto_term.ML"
+use "Tools/Function/relation.ML"
 use "Tools/Function/function.ML"
 use "Tools/Function/pat_completeness.ML"
 use "Tools/Function/fun.ML"
diff -r b8cdd3d73022 -r acc2bd3934ba src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Oct 23 16:22:10 2009 +0200
+++ b/src/HOL/IsaMakefile	Fri Oct 23 16:37:56 2009 +0200
@@ -156,7 +156,6 @@
   Tools/Datatype/datatype_realizer.ML \
   Tools/Datatype/datatype_rep_proofs.ML \
   Tools/dseq.ML \
-  Tools/Function/auto_term.ML \
   Tools/Function/context_tree.ML \
   Tools/Function/decompose.ML \
   Tools/Function/descent.ML \
@@ -172,6 +171,7 @@
   Tools/Function/mutual.ML \
   Tools/Function/pat_completeness.ML \
   Tools/Function/pattern_split.ML \
+  Tools/Function/relation.ML \
   Tools/Function/scnp_reconstruct.ML \
   Tools/Function/scnp_solve.ML \
   Tools/Function/size.ML \
diff -r b8cdd3d73022 -r acc2bd3934ba src/HOL/Tools/Function/auto_term.ML
--- a/src/HOL/Tools/Function/auto_term.ML	Fri Oct 23 16:22:10 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-(*  Title:      HOL/Tools/Function/auto_term.ML
-    Author:     Alexander Krauss, TU Muenchen
-
-A package for general recursive function definitions.
-Method "relation" to commence a termination proof using a user-specified relation.
-*)
-
-signature FUNCTION_RELATION =
-sig
-  val relation_tac: Proof.context -> term -> int -> tactic
-  val setup: theory -> theory
-end
-
-structure Function_Relation : FUNCTION_RELATION =
-struct
-
-fun inst_thm ctxt rel st =
-    let
-      val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
-      val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
-      val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st
-      val Rvar = cert (Var (the_single (Term.add_vars (prop_of st') [])))
-    in 
-      Drule.cterm_instantiate [(Rvar, rel')] st' 
-    end
-
-fun relation_tac ctxt rel i = 
-    TRY (Function_Common.apply_termination_rule ctxt i)
-    THEN PRIMITIVE (inst_thm ctxt rel)
-
-val setup =
-  Method.setup @{binding relation}
-    (Args.term >> (fn rel => fn ctxt => SIMPLE_METHOD' (relation_tac ctxt rel)))
-    "proves termination using a user-specified wellfounded relation"
-
-end
diff -r b8cdd3d73022 -r acc2bd3934ba src/HOL/Tools/Function/relation.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Function/relation.ML	Fri Oct 23 16:37:56 2009 +0200
@@ -0,0 +1,36 @@
+(*  Title:      HOL/Tools/Function/relation.ML
+    Author:     Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions.
+Method "relation" to commence a termination proof using a user-specified relation.
+*)
+
+signature FUNCTION_RELATION =
+sig
+  val relation_tac: Proof.context -> term -> int -> tactic
+  val setup: theory -> theory
+end
+
+structure Function_Relation : FUNCTION_RELATION =
+struct
+
+fun inst_thm ctxt rel st =
+    let
+      val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
+      val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
+      val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st
+      val Rvar = cert (Var (the_single (Term.add_vars (prop_of st') [])))
+    in 
+      Drule.cterm_instantiate [(Rvar, rel')] st' 
+    end
+
+fun relation_tac ctxt rel i = 
+    TRY (Function_Common.apply_termination_rule ctxt i)
+    THEN PRIMITIVE (inst_thm ctxt rel)
+
+val setup =
+  Method.setup @{binding relation}
+    (Args.term >> (fn rel => fn ctxt => SIMPLE_METHOD' (relation_tac ctxt rel)))
+    "proves termination using a user-specified wellfounded relation"
+
+end