relation method: re-check given term with type constraints to avoid unspecific failure if ill-typed -- keep old behaviour for tactic version

--- a/src/HOL/Tools/Function/relation.ML	Fri Oct 22 12:01:12 2010 +0200
+++ b/src/HOL/Tools/Function/relation.ML	Fri Oct 22 13:59:34 2010 +0200
@@ -14,24 +14,32 @@
 structure Function_Relation : FUNCTION_RELATION =
 struct
 
-fun inst_state_tac 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
-  in case Term.add_vars (prop_of st') [] of
-       [v] => 
-         PRIMITIVE (Drule.cterm_instantiate [(cert (Var v), rel')]) st'
-     | _ => Seq.empty
-  end
+fun gen_inst_state_tac prep 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'
+      end
+  | _ => Seq.empty;
 
-fun relation_tac ctxt rel i =
+fun gen_relation_tac prep ctxt rel i =
   TRY (Function_Common.apply_termination_rule ctxt i)
-  THEN inst_state_tac ctxt rel
+  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)
 
 val setup =
-  Method.setup @{binding relation}
-    (Args.term >> (fn rel => fn ctxt => SIMPLE_METHOD' (relation_tac ctxt rel)))
+  Method.setup @{binding relation} (Args.term >> relation_meth)
     "proves termination using a user-specified wellfounded relation"
 
 end