# HG changeset patch
# User krauss
# Date 1287748774 -7200
# Node ID b237f757b215158808841ab8d0a6563c617dded9
# Parent  0bee30e3a4ad67925564d55dabeb3b1223f75a3f
relation method: re-check given term with type constraints to avoid unspecific failure if ill-typed -- keep old behaviour for tactic version

diff -r 0bee30e3a4ad -r b237f757b215 src/HOL/Tools/Function/relation.ML
--- 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