# HG changeset patch
# User krauss
# Date 1289253740 -3600
# Node ID 65bd37d7d5010d8e158214887539a3afa1da8a65
# Parent  19faffbe50660b3e2e77bedb33e65e8d520e6124
removed type-inference-like behaviour from relation_tac completely; tuned

diff -r 19faffbe5066 -r 65bd37d7d501 src/HOL/Tools/Function/relation.ML
--- a/src/HOL/Tools/Function/relation.ML	Mon Nov 08 17:44:47 2010 +0100
+++ b/src/HOL/Tools/Function/relation.ML	Mon Nov 08 23:02:20 2010 +0100
@@ -7,39 +7,50 @@
 
 signature FUNCTION_RELATION =
 sig
-  val relation_tac: Proof.context -> term -> int -> tactic
+  val relation_tac: Proof.context -> (typ -> term) -> int -> tactic
   val setup: theory -> theory
 end
 
 structure Function_Relation : FUNCTION_RELATION =
 struct
 
-fun gen_inst_state_tac prep ctxt rel st =
+(* tactic version *)
+
+fun inst_state_tac inst st =
+  case Term.add_vars (prop_of st) [] of
+    [v as (_, T)] =>
+      let val cert = Thm.cterm_of (Thm.theory_of_thm st);
+      in PRIMITIVE (Thm.instantiate ([], [(cert (Var v), cert (inst T))])) st end
+  | _ => Seq.empty;
+
+fun relation_tac ctxt rel i =
+  TRY (Function_Common.apply_termination_rule ctxt i)
+  THEN inst_state_tac rel;
+
+
+(* method version (with type inference) *)
+
+fun inst_state_infer_tac ctxt rel st =
   case Term.add_vars (prop_of st) [] of
     [v as (_, T)] =>
       let
-        val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
-        val rel' = prep T (singleton (Variable.polymorphic ctxt) rel) 
-          |> cert
-        val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st (*FIXME??*)
-      in        
-        PRIMITIVE (Drule.cterm_instantiate [(cert (Var v), rel')]) st'
+        val cert = Thm.cterm_of (ProofContext.theory_of ctxt);
+        val rel' = singleton (Variable.polymorphic ctxt) rel
+          |> map_types Type_Infer.paramify_vars
+          |> Type.constraint T
+          |> Syntax.check_term ctxt
+          |> cert;
+      in
+        PRIMITIVE (Thm.instantiate ([], [(cert (Var v), rel')])) st
       end
   | _ => Seq.empty;
 
-fun gen_relation_tac prep ctxt rel i =
+fun relation_meth rel ctxt = SIMPLE_METHOD' (fn i =>
   TRY (Function_Common.apply_termination_rule ctxt i)
-  THEN gen_inst_state_tac prep ctxt rel
-
-val relation_tac = gen_relation_tac (K I)
-
-fun relation_meth rel ctxt = SIMPLE_METHOD' 
-  (gen_relation_tac (fn T => map_types Type_Infer.paramify_vars
-      #> Type.constraint T #> Syntax.check_term ctxt)
-    ctxt rel)
+  THEN inst_state_infer_tac ctxt rel);
 
 val setup =
   Method.setup @{binding relation} (Args.term >> relation_meth)
-    "proves termination using a user-specified wellfounded relation"
+    "proves termination using a user-specified wellfounded relation";
 
 end